tab -> ' '

[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 5e02fdbaaa391d00705586a0df49d61d60b79a2a..1499712c925e26dd527bd8878a79d5812be42a78 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicReduction.ml
+++ b/helm/software/components/cic_proof_checking/cicReduction.ml
@@ -869,19 +869,26 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1);
 *)
                aux test_equality_only context t1 term' ugraph
             with  CicUtil.Subst_not_found _ -> false,ugraph)
-          (* TASSI: CONSTRAINTS *)
-        | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
+        | (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)
-          (* TASSI: CONSTRAINTS *)
-        | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
+        | (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)
-          (* TASSI: CONSTRAINTS *)
-        | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph
-          (* TASSI: CONSTRAINTS *)
+        | (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 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
         | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
             let b',ugraph' = aux true context s1 s2 ugraph in