From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 26 Jul 2005 12:04:16 +0000 (+0000)
Subject: Bug fixed: list_uniq o List.sort used in the lookup function to return only
X-Git-Tag: V_0_7_2~70
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=aa05519b7416dbd248f05119cce3cb4091098c7d;p=helm.git

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 8c73f8407..e54d5b481 100644
--- 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 =