From a712ca1da0bf5ffdcaef74e65fc3a71ba800873f Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 5 Jun 2019 19:15:29 +0200
Subject: [PATCH] [kernel] document new Logic_info_structural datatype

---
 src/kernel_services/ast_queries/cil_datatype.mli | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/src/kernel_services/ast_queries/cil_datatype.mli b/src/kernel_services/ast_queries/cil_datatype.mli
index 9e98b281b8e..4535cdea3c4 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
 
-- 
GitLab