avoid generating multiple times the same xref/href

[helm.git] / helm / ocaml / cic_notation / cicNotationRew.ml

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index b5d3d271dbd798880fa947b15b4652c660be9fed..28edd491c84e7e32e97425176cb728e007e723e3 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -87,7 +87,8 @@ let vbox = box Ast.V
 let hvbox = box Ast.HV
 let hovbox = box Ast.HOV
 let break = Ast.Layout Ast.Break
-let reset_href t = Ast.AttributedTerm (`Href [], t)
+(* let reset_href t = Ast.AttributedTerm (`Href [], t) *)
+let reset_href t = t
 let builtin_symbol s = reset_href (Ast.Literal (`Symbol s))
 let keyword k = reset_href (add_keyword_attrs (Ast.Literal (`Keyword k)))
 let number s =
@@ -259,7 +260,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