From 5813d9a88f34f0c0d15cb74243f638d02ae163fa Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 10 Mar 2007 22:23:38 +0000 Subject: [PATCH] rewrite tactic: bug fix in rewriting under Pi's: the application context of the subterm to rewrite can not be forgotten --- components/tactics/equalityTactics.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/components/tactics/equalityTactics.ml b/components/tactics/equalityTactics.ml index b445dfb86..a31b0f052 100644 --- a/components/tactics/equalityTactics.ml +++ b/components/tactics/equalityTactics.ml @@ -149,7 +149,9 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality = match concl_pat with | None -> None | Some term -> Some (S.lift 1 term) in - Some (fun _ m u -> lifted_t1, m, u),[],lifted_concl_pat + Some (fun c m u -> + let distance = pred (List.length c - List.length context) in + S.lift distance lifted_t1, m, u),[],lifted_concl_pat in let subst,metasenv',ugraph,_,selected_terms_with_context = ProofEngineHelpers.select -- 2.39.2