From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 29 Apr 2005 12:13:05 +0000 (+0000)
Subject: catched UniverseInconsistency
X-Git-Tag: single_binding~135
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=722256712b8b0c6acc08a36fa6c9cde8cc5ecc4b;p=helm.git

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 552e3d30b..bb70ce279 100644
--- 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