From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 28 Jul 2005 10:48:26 +0000 (+0000)
Subject: workaround for an assertion failure during rendering (missing sort of some ids)
X-Git-Tag: V_0_7_2~23
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d02c611bd8da3ea28305958fd9ec4798f20d56d8;p=helm.git

workaround for an assertion failure during rendering (missing sort of some ids)
---

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