X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationRew.ml;h=dba599fc895fcafc01cd999b26927edbaa259c4e;hb=3535b8c86ed85f10ae9b25ad449e1d0aaeccc90a;hp=e54d5b48152098e8b33ffcec7a316a9a6d98a49a;hpb=aa05519b7416dbd248f05119cce3cb4091098c7d;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index e54d5b481..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))