From f82a5324071bc1b8fc5c9ea95ba03e40801c74ed Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 21 May 2002 15:24:22 +0000 Subject: [PATCH] Two Meta occurrences where a parameter is accessible only in one of them can now be considered convertible. --- helm/ocaml/cic_proof_checking/cicReductionNaif.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml index fbfe21c44..86e58aa9f 100644 --- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml +++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml @@ -212,9 +212,9 @@ let are_convertible = (fun b t1 t2 -> b && match t1,t2 with - None,None -> true + None,_ + | _,None -> true | Some t1',Some t2' -> aux context t1' t2' - | _,_ -> false ) true l1 l2 | (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *) | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) -> -- 2.39.2