diff --git a/src/kernel_internals/typing/allocates.mli b/src/kernel_internals/typing/allocates.mli
index 8e03dec87599f7dd73882a6a401822fbfc28fd29..db5e15c991b84372b92ac48aafae25ab6d493b2e 100644
--- a/src/kernel_internals/typing/allocates.mli
+++ b/src/kernel_internals/typing/allocates.mli
@@ -20,7 +20,12 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(** Generation of default [allocates \nothing] clauses. *)
+(** Generation of default [allocates \nothing] clauses.
+
+    Automatic generation of [allocates \nothing] and [loop allocates \nothing]
+    clauses has been removed until a plugin supports them.
+    To force generation, the following functions can be used.
+*)
 
 val add_allocates_nothing_funspec: Cil_types.kernel_function -> unit
 (** Adds [allocates \nothing] to the default behavior of the function