Bug fixed: list_uniq o List.sort used in the lookup function to return only

one interpretation in case of duplicate interpretation definitions. This
happens when a module A defines an interpretation, it is included by B and
C and then a module D includes both B and C, thus defining the interpretation
twice.

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index 8c73f84072fa070b332a0ed33644e8a3ae2cdee7..e54d5b48152098e8b33ffcec7a316a9a6d98a49a 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -569,9 +569,17 @@ let add_interpretation dsc (symbol, args) appl_pattern =
 exception Interpretation_not_found
 exception Pretty_printer_not_found
 
+let rec list_uniq = function 
+  | [] -> []
+  | h::[] -> [h]
+  | h1::h2::tl when h1 = h2 -> list_uniq (h2 :: tl) 
+  | h1::tl (* when h1 <> h2 *) -> h1 :: list_uniq tl
+
 let lookup_interpretations symbol =
   try
-    List.map
+   list_uniq
+    (List.sort Pervasives.compare
+     (List.map
       (fun id ->
         let (dsc, _, args, appl_pattern, _) =
           try
@@ -579,7 +587,7 @@ let lookup_interpretations symbol =
           with Not_found -> assert false 
         in
         dsc, args, appl_pattern)
-      !(Hashtbl.find interpretations symbol)
+      !(Hashtbl.find interpretations symbol)))
   with Not_found -> raise Interpretation_not_found
 
 let add_pretty_printer ~precedence ~associativity l2 l1 =