UniverseInconsistency is now wrapper by CicRefine.type_of_aux' to RefineFailure

[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.ml

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