X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicReduction.ml;h=f4880e426de66ffd74b78808eea763cb4b761a71;hb=fc1e25e37ba7deb07572f0cdb63aef02f0468dcb;hp=b636c2a729aa2ef688d99a8c8a42e0c173b795f5;hpb=bada8520939f45188270ba7ba5e006e55d3a0d15;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml
index b636c2a72..f4880e426 100644
--- a/helm/software/components/cic_proof_checking/cicReduction.ml
+++ b/helm/software/components/cic_proof_checking/cicReduction.ml
@@ -856,10 +856,14 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1);
             with  CicUtil.Subst_not_found _ -> false,ugraph)
           (* TASSI: CONSTRAINTS *)
         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
-            true,(CicUniv.add_eq t2 t1 ugraph)
+            (try
+              true,(CicUniv.add_eq t2 t1 ugraph)
+             with CicUniv.UniverseInconsistency _ -> false,ugraph)
           (* TASSI: CONSTRAINTS *)
         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
-            true,(CicUniv.add_ge t2 t1 ugraph)
+            (try
+              true,(CicUniv.add_ge t2 t1 ugraph)
+             with CicUniv.UniverseInconsistency _ -> false,ugraph)
           (* TASSI: CONSTRAINTS *)
         | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph
           (* TASSI: CONSTRAINTS *)