X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReductionMachine.ml;h=e963ddce9b5062a941a45ff2b6e3cf44c89b8707;hb=bb236c2ac110124de92fa2d0fb2882d273a7f7eb;hp=751f96be04576435d472f6f99973fa7bff3ccf52;hpb=182b62080ee70e53d8bd188613e25244345489f9;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
index 751f96be0..e963ddce9 100644
--- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
@@ -802,8 +802,17 @@ let are_convertible =
                   | _,None  -> true
                   | Some t1',Some t2' -> aux test_equality_only context t1' t2'
               ) true l1 l2
-        | (C.Sort s1, C.Sort s2) when s1 = s2 || s2 = C.Type -> true
-        | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
+	  (* TASSI: CONSTRAINTS *)
+	| (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
+	    CicUniv.add_eq t2 t1
+	  (* TASSI: CONSTRAINTS *)
+	| (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
+	    CicUniv.add_ge t2 t1
+	  (* TASSI: CONSTRAINTS *)
+	| (C.Sort s1, C.Sort (C.Type _)) -> not test_equality_only
+	  (* TASSI: CONSTRAINTS *)
+        | (C.Sort s1, C.Sort s2) -> s1 = s2
+	| (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
            aux true context s1 s2 &&
             aux test_equality_only ((Some (name1, (C.Decl s1)))::context) t1 t2
         | (C.Lambda (name1,s1,t1), C.Lambda(_,s2,t2)) ->