X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdisambiguate.ml;h=570ab894e434e7b9f45b5444e854c14b09fda6fe;hb=a6dd077a2b3e4d0c4395c2ee4cc2e1b6d10ab963;hp=bb70ce279bdaf2ba376a784a666d52c7d758c5ef;hpb=722256712b8b0c6acc08a36fa6c9cde8cc5ecc4b;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index bb70ce279..570ab894e 100644
--- 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