]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_notation/cicNotationRew.ml
workaround for an assertion failure during rendering (missing sort of some ids)
[helm.git] / helm / ocaml / cic_notation / cicNotationRew.ml
index b5d3d271dbd798880fa947b15b4652c660be9fed..dba599fc895fcafc01cd999b26927edbaa259c4e 100644 (file)
@@ -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