diff --git a/src/kernel_services/ast_queries/cil_datatype.ml b/src/kernel_services/ast_queries/cil_datatype.ml
index f0b07d285acea344d7019b658055959dad311526..86342ad91af642bd70d13ad73f8c8fa60a271444 100644
--- a/src/kernel_services/ast_queries/cil_datatype.ml
+++ b/src/kernel_services/ast_queries/cil_datatype.ml
@@ -1357,6 +1357,48 @@ let rec hash_logic_type config = function
   | Larrow (_,t) -> 41 * hash_logic_type config t
 
 
+(* Logic_info with structural comparison
+   if functions / predicates have the same name (overloading), compare
+   their arguments types ; ignore polymorphism *)
+module Logic_info_structural = struct
+  let pretty_ref = ref (fun fmt f -> Logic_var.pretty fmt f.l_var_info)
+  include  Make_with_collections
+    (struct
+      type t = logic_info
+      let name = "Logic_info_structural"
+      let reprs =
+	List.map
+	  (fun v ->
+	    { l_var_info = v;
+	      l_labels = [];
+	      l_tparams = [];
+	      l_type = None;
+	      l_profile = [];
+	      l_body = LBnone })
+	  Logic_var.reprs
+      let compare i1 i2 =
+        let name_cmp =
+          String.compare i1.l_var_info.lv_name i2.l_var_info.lv_name
+        in
+        if name_cmp <> 0 then name_cmp else begin
+          let config =
+            { by_name = true ; logic_type = true ; unroll = true }
+          in
+          let prm_cmp p1 p2 =
+            compare_logic_type config p1.lv_type p2.lv_type
+          in
+          compare_list prm_cmp i1.l_profile i2.l_profile
+        end
+
+      let equal = Datatype.from_compare
+      let hash i = Logic_var.hash i.l_var_info
+      let copy = Datatype.undefined
+      let internal_pretty_code = Datatype.undefined
+      let pretty = !pretty_ref
+      let varname _ = "logic_varinfo"
+     end)
+end
+
 (* Shared between the different modules for logic types *)
 let pretty_logic_type_ref = ref (fun _ _ -> assert false)
 
diff --git a/src/kernel_services/ast_queries/cil_datatype.mli b/src/kernel_services/ast_queries/cil_datatype.mli
index 983c6ba3a370e057864d950511d64e919eea8f9d..4535cdea3c4e929b7622088615189bbccdad457d 100644
--- a/src/kernel_services/ast_queries/cil_datatype.mli
+++ b/src/kernel_services/ast_queries/cil_datatype.mli
@@ -256,6 +256,17 @@ 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
 
 module Logic_label: S_with_collections_pretty with type t = logic_label
diff --git a/src/libraries/stdlib/extlib.ml b/src/libraries/stdlib/extlib.ml
index 8e5d2022b9ead6818cc53c369c0a4f79d9f6d72a..f815f104a071411a50b6eb1501f1b29853fe773e 100644
--- a/src/libraries/stdlib/extlib.ml
+++ b/src/libraries/stdlib/extlib.ml
@@ -127,8 +127,8 @@ let rec list_compare cmp_elt l1 l2 =
   else
     match l1, l2 with
       | [], [] -> assert false (* included in l1 == l2 above *)
-      | [], _ :: _ -> 1
-      | _ :: _, [] -> -1
+      | [], _ :: _ -> -1
+      | _ :: _, [] -> 1
       | v1::r1, v2::r2 ->
           let c = cmp_elt v1 v2 in
           if c = 0 then list_compare cmp_elt r1 r2 else c