diff --git a/src/kernel_services/ast_queries/cil_datatype.mli b/src/kernel_services/ast_queries/cil_datatype.mli
index 9e98b281b8ed6839bf5a54088ffbee492d982cbf..4535cdea3c4e929b7622088615189bbccdad457d 100644
--- a/src/kernel_services/ast_queries/cil_datatype.mli
+++ b/src/kernel_services/ast_queries/cil_datatype.mli
@@ -256,6 +256,16 @@ module Identified_term: S_with_collections_pretty with type t = identified_term
 
 module Logic_ctor_info: S_with_collections_pretty with type t = logic_ctor_info
 module Logic_info: S_with_collections_pretty with type t = logic_info
+
+(** Logic_info with structural comparison:
+    - name of the symbol
+    - type of arguments
+    Note that polymorphism is ignored, in the sense that two symbols with
+    the same name and profile except for the name of their type variables
+    will compare unequal.
+
+    @since Frama-C+dev
+*)
 module Logic_info_structural: S_with_collections_pretty with type t = logic_info
 module Logic_constant: S_with_collections_pretty with type t = logic_constant