X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationRew.ml;h=dba599fc895fcafc01cd999b26927edbaa259c4e;hb=b9af9f1c0de6a1735b492f5c793a87a8fce218cc;hp=8c73f84072fa070b332a0ed33644e8a3ae2cdee7;hpb=08ecc780b3b0a4cac7ed72cf68c310e4eeffa2c1;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index 8c73f8407..dba599fc8 100644
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -259,7 +259,9 @@ let ast_of_acic0 term_info acic k =
   let sort_of_id id =
     try
       Hashtbl.find term_info.sort id
-    with Not_found -> assert false
+    with Not_found ->
+      prerr_endline (sprintf "warning: sort of id %s not found, using Type" id);
+      `Type
   in
   let aux_substs substs =
     Some
@@ -529,9 +531,10 @@ let rec ast_of_acic1 term_info annterm =
         with Not_found -> assert false
       in
       let ast = instantiate32 term_info env' symbol args in
-      match uris with
-      | [] -> ast
-      | _ -> Ast.AttributedTerm (`Href uris, ast)
+      Ast.AttributedTerm (`IdRef (CicUtil.id_of_annterm annterm),
+        (match uris with
+        | [] -> ast
+        | _ -> Ast.AttributedTerm (`Href uris, ast)))
 
 let load_patterns32 t =
   set_compiled32 (lazy (CicNotationMatcher.Matcher32.compiler t))
@@ -569,9 +572,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 +590,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 =