From 80d680bbbd13116576c961508e3c5631f218308d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 2 Jul 2004 15:34:35 +0000 Subject: [PATCH] Bug fixed: eta_expand did not perform any recursion over the local context of a metavariable ==> the local context was not lifted. --- helm/ocaml/tactics/primitiveTactics.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index cc743d7cc..e318bd87c 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -72,7 +72,11 @@ let eta_expand metasenv context t arg = | C.Var (uri,exp_named_subst) -> let exp_named_subst' = aux_exp_named_subst n exp_named_subst in C.Var (uri,exp_named_subst') - | C.Meta _ + | C.Meta (i,l) -> + let l' = + List.map (function None -> None | Some t -> Some (aux n t)) l + in + C.Meta (i, l') | C.Sort _ | C.Implicit _ as t -> t | C.Cast (te,ty) -> C.Cast (aux n te, aux n ty) -- 2.39.2