From 3db0a84a64f014fa10c4b439c62cb3eef017ea7a Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 5 Jul 2004 07:12:30 +0000 Subject: [PATCH] Bug fixed: beta_expand did not perform any recursion over the local context of a metavariable ==> the local context was not lifted. --- helm/ocaml/cic_unification/cicUnification.ml | 20 ++++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 646670ec8..e6213d6af 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -67,8 +67,20 @@ let rec beta_expand test_equality_only metasenv subst context t arg = (try let (_, t') = CicMetaSubst.lookup_subst i subst in aux metasenv subst n context (CicSubstitution.lift_meta l t') - with - CicMetaSubst.SubstNotFound _ -> subst,metasenv,t) + with CicMetaSubst.SubstNotFound _ -> + let (subst, metasenv, context, local_context) = + List.fold_left + (fun (subst, metasenv, context, local_context) t -> + match t with + | None -> (subst, metasenv, context, None :: local_context) + | Some t -> + let (subst, metasenv, t) = + aux metasenv subst n context t + in + (subst, metasenv, context, Some t :: local_context)) + (subst, metasenv, context, []) l + in + (subst, metasenv, C.Meta (i, local_context))) | C.Sort _ | C.Implicit _ as t -> subst,metasenv,t | C.Cast (te,ty) -> @@ -387,8 +399,8 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; fo_unif_subst test_equality_only subst context metasenv h1 h2 | ([h],l) | (l,[h]) -> - fo_unif_subst - test_equality_only subst context metasenv h (C.Appl (List.rev l)) + fo_unif_subst test_equality_only subst context metasenv + h (C.Appl (List.rev l)) | ((h1::l1),(h2::l2)) -> let subst', metasenv' = fo_unif_subst test_equality_only subst context metasenv h1 h2 -- 2.39.2