catched UniverseInconsistency

(only an hack, it should be wrapped by the refiner)

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 552e3d30b21898eb7596194b6a7c3f7d4c263d8f..bb70ce279bdaf2ba376a784a666d52c7d758c5ef 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -73,9 +73,13 @@ let refine metasenv context term ugraph =
           debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
             (CicPp.ppterm term) msg);
           Ko,ugraph
-      | CicUnification.UnificationFailure s -> 
-        prerr_endline ("PASSADI QUI: " ^ s);
-          raise ( CicUnification.UnificationFailure s )
+      | CicUniv.UniverseInconsistency s ->
+         prerr_endline (
+           "INTERPRETAZIONE FALLITA PER UNIVERSE INCONSISTENCY:\n" ^ s);
+           (* non mi e' chiaro se debba essere wrappata dal typechecker o dal
+            * refiner, in ogni caso non andrebbe qui 
+            *)
+         Ko, ugraph
 
 let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () =
   try