diff --git a/theories/functions.v b/theories/functions.v
index 60dbdb2051f977af0544b46f7d0f4e3c989c3fc0..ebc83e2d16f2e3bcb51bb6e346c3b37418d239d1 100644
--- a/theories/functions.v
+++ b/theories/functions.v
@@ -8,7 +8,7 @@ Section definitions.
     λ (g : T → T) a f b, if decide (a = b) then g (f a) else f b.
 End definitions.
 
-(* For now, we only have the properties here that do not need a notion
+(* TODO: For now, we only have the properties here that do not need a notion
    of equality of functions. *)
 
 Section functions.