X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReductionNaif.ml;h=95f24ebf39d6963bfc9df75e16873eefac315126;hb=c5d5bf37b1e4c4b9b499ed2cbfe27cf2ec181944;hp=ea7fb42298adcc2543dd42e1b786ac05510fe08e;hpb=515c95d5d339bc457772d3dd08765b55ad140054;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml index ea7fb4229..95f24ebf3 100644 --- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml +++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml @@ -215,7 +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 || 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