X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicReduction.ml;h=ff19dff194bf2720b6f2ba6aaadaa74bad6f7efb;hb=0b76904a3f10bfd6390d26172fd6979626bd72f4;hp=5e02fdbaaa391d00705586a0df49d61d60b79a2a;hpb=d344d41028275b6d1451dca8e40a88e33e588389;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml
index 5e02fdbaa..ff19dff19 100644
--- a/helm/software/components/cic_proof_checking/cicReduction.ml
+++ b/helm/software/components/cic_proof_checking/cicReduction.ml
@@ -869,19 +869,16 @@ 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 ->
-            (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)) ->
-            (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.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
         | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
             let b',ugraph' = aux true context s1 s2 ugraph in