CProp_i <= Type_i , Type_i <= CProp_i

[helm.git] / helm / software / components / cic_proof_checking / cicReduction.ml

diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml
index 1499712c925e26dd527bd8878a79d5812be42a78..ff19dff194bf2720b6f2ba6aaadaa74bad6f7efb 100644 (file)
--- 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