Universes introduction

[helm.git] / helm / ocaml / cic_proof_checking / cicReductionNaif.ml

diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
index 033614eeae21fff6f42227e5020b7452221b61b5..95f24ebf39d6963bfc9df75e16873eefac315126 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
@@ -215,9 +215,16 @@ 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 || (not test_equality_only) && s2 = C.Type
-           -> true
+          (* 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