From 3b501e4d3e53e02cd901aa6ee08bb848579be59c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 16 Apr 2004 17:15:35 +0000 Subject: [PATCH] test_equality_only was not used in sort comparison. It should be implemented only in unification. --- helm/ocaml/cic_proof_checking/cicReductionMachine.ml | 4 +++- helm/ocaml/cic_proof_checking/cicReductionNaif.ml | 4 +++- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml index 751f96be0..4ef3ce940 100644 --- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml +++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml @@ -802,7 +802,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 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 -- 2.39.2