CicUniv.UniverseInconsistency is no handled correcly.

[helm.git] / helm / software / components / cic_unification / cicRefine.ml

diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index dee8ba5f3a451d7e8470f738fbabf618397314d9..21af1f9c74533cb640311e630c61fac70ffa0f96 100644 (file)
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/components/cic_unification/cicRefine.ml
@@ -395,8 +395,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                    subst', metasenv',ugraph1)
         | C.Sort (C.Type tno) -> 
             let tno' = CicUniv.fresh() in 
-            let ugraph1 = CicUniv.add_gt tno' tno ugraph in
-              t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
+             (try
+               let ugraph1 = CicUniv.add_gt tno' tno ugraph in
+                 t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
+              with
+               CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
         | C.Sort _ -> 
             t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
         | C.Implicit infos ->
@@ -1145,9 +1148,12 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il
               C.Sort s2,subst,metasenv,ugraph
         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) -> 
             let t' = CicUniv.fresh() in 
-            let ugraph1 = CicUniv.add_ge t' t1 ugraph in
-            let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
-              C.Sort (C.Type t'),subst,metasenv,ugraph2
+             (try
+              let ugraph1 = CicUniv.add_ge t' t1 ugraph in
+              let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
+                C.Sort (C.Type t'),subst,metasenv,ugraph2
+              with
+               CicUniv.UniverseInconsistency msg -> raise (RefineFailure msg))
         | (C.Sort _,C.Sort (C.Type t1)) -> 
             C.Sort (C.Type t1),subst,metasenv,ugraph
         | (C.Meta _, C.Sort _) -> t2'',subst,metasenv,ugraph