X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReductionNaif.ml;h=033614eeae21fff6f42227e5020b7452221b61b5;hp=ea7fb42298adcc2543dd42e1b786ac05510fe08e;hb=3b501e4d3e53e02cd901aa6ee08bb848579be59c;hpb=86c7cb1e030964d7d3ca09ac52f7f572b02f1af4

diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
index ea7fb4229..033614eea 100644
--- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
@@ -215,7 +215,9 @@ 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.Sort s1, C.Sort s2) when
+             s1 = s2 || (not test_equality_only) && s2 = C.Type
+           -> true
         | (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