From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 21 May 2002 15:24:22 +0000 (+0000)
Subject: Two Meta occurrences where a parameter is accessible only in one of them
X-Git-Tag: V_0_3_0_debian_8~90
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=f82a5324071bc1b8fc5c9ea95ba03e40801c74ed

Two Meta occurrences where a parameter is accessible only in one of them
can now be considered convertible.
---

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)) ->