X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicReduction.ml;h=ff19dff194bf2720b6f2ba6aaadaa74bad6f7efb;hb=0b15dfdee3357a626c77d30599e87a83ab34e471;hp=1499712c925e26dd527bd8878a79d5812be42a78;hpb=6719c0e318b312b51b089fea3d69d1b7103245ea;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml
index 1499712c9..ff19dff19 100644
--- a/helm/software/components/cic_proof_checking/cicReduction.ml
+++ b/helm/software/components/cic_proof_checking/cicReduction.ml
@@ -869,24 +869,14 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1);
 *)
                aux test_equality_only context t1 term' ugraph
             with  CicUtil.Subst_not_found _ -> false,ugraph)
-        | (C.Sort (C.Type t1), C.Sort (C.Type t2)) 
-        | (C.Sort (C.CProp t1), C.Sort (C.CProp t2)) when test_equality_only ->
-            (try
-              true,(CicUniv.add_eq t2 t1 ugraph)
-             with CicUniv.UniverseInconsistency _ -> false,ugraph)
-        | (C.Sort (C.Type t1), C.Sort (C.Type t2)) 
-        | (C.Sort (C.CProp t1), C.Sort (C.CProp t2)) ->
-            (try
-              true,(CicUniv.add_ge t2 t1 ugraph)
-             with CicUniv.UniverseInconsistency _ -> false,ugraph)
-        | (C.Sort (C.CProp t1), C.Sort (C.Type t2)) when not test_equality_only ->
-            (try
-              true,(CicUniv.add_gt t2 t1 ugraph)
-             with CicUniv.UniverseInconsistency _ -> false,ugraph)
-        | (C.Sort (C.Type t1), C.Sort (C.CProp t2)) when not test_equality_only ->
-            (try
-              true,(CicUniv.add_ge t2 t1 ugraph)
-             with CicUniv.UniverseInconsistency _ -> false,ugraph)
+        | (C.Sort (C.CProp t1|C.Type t1), C.Sort (C.CProp t2|C.Type t2)) 
+          when test_equality_only ->
+            (try true,(CicUniv.add_eq t2 t1 ugraph)
+            with CicUniv.UniverseInconsistency _ -> false,ugraph)
+        | (C.Sort (C.CProp t1|C.Type t1), C.Sort (C.CProp t2|C.Type t2))
+          when not test_equality_only ->
+            (try true,(CicUniv.add_ge t2 t1 ugraph)
+            with CicUniv.UniverseInconsistency _ -> false,ugraph)
         | (C.Sort s1, C.Sort (C.Type _))
         | (C.Sort s1, C.Sort (C.CProp _)) -> (not test_equality_only),ugraph
         | (C.Sort s1, C.Sort s2) -> (s1 = s2),ugraph