diff --git a/src/plugins/wp/Sigs.ml b/src/plugins/wp/Sigs.ml
index 0e82aeb893bdbbd14f660cbcab6659c78cd4c42c..1b594803754f617a5c0b63f94f1216275517fed2 100644
--- a/src/plugins/wp/Sigs.ml
+++ b/src/plugins/wp/Sigs.ml
@@ -612,8 +612,10 @@ sig
 
         Remark: [None] initializer are interpreted as zeroes. This is consistent
         with the [init option] associated with global variables in CIL,
-        for which the default initializer are zeroes. There is no
-        [init option] value associated with local initializers.
+        for which the default initializer are zeroes. This function is called
+        for global initializers and local initializers ([Cil.Local_init]).
+        It is not called for local variables without initializers as they do not
+        have a [Cil.init option].
     *)
 
 end