X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReductionMachine.ml;h=4aee1b2b922292ae8a2998bc9a63582123eb263e;hb=12a55c7dd3cb44f7a4586524d5e342966bcfae60;hp=dbe22fb3e6ceb107b7d77d7af1d57fecb2e213df;hpb=8683d424a209bce154263e31f78c600d20753236;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
index dbe22fb3e..4aee1b2b9 100644
--- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
@@ -802,7 +802,7 @@ let are_convertible =
                   | _,None  -> true
                   | Some t1',Some t2' -> aux context t1' t2'
               ) true l1 l2
-        | (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *)
+        | (C.Sort s1, C.Sort s2) when s1 = s2 || s2 = C.Type -> true
         | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->
            aux context s1 s2 &&
             aux ((Some (name1, (C.Decl s1)))::context) t1 t2