UniverseInconsistency is now wrapper by CicRefine.type_of_aux' to RefineFailure

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index bb70ce279bdaf2ba376a784a666d52c7d758c5ef..570ab894e434e7b9f45b5444e854c14b09fda6fe 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -73,13 +73,6 @@ let refine metasenv context term ugraph =
           debug_print (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
             (CicPp.ppterm term) msg);
           Ko,ugraph
-      | 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

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index c5f775253a004bce33c6ea393fb5f3877dfa52d6..4a6e6cadf798ef6fd16c154da24d513a4520a968 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -880,6 +880,13 @@ and type_of_aux' metasenv context t ugraph =
     (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1) 
 ;;
 
+let type_of_aux' metasenv context term ugraph =
+  try 
+    type_of_aux' metasenv context term ugraph
+  with 
+    CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg)
+    
+
 (* DEBUGGING ONLY 
 let type_of_aux' metasenv context term =
  try