From 5cf27f4cc19d59ed91cda9d8ec7d702c32384378 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 10 Mar 2007 22:23:38 +0000 Subject: [PATCH 1/1] rewrite tactic: bug fix in rewriting under Pi's: the application context of the subterm to rewrite can not be forgotten --- helm/software/components/tactics/equalityTactics.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/helm/software/components/tactics/equalityTactics.ml b/helm/software/components/tactics/equalityTactics.ml index b445dfb86..a31b0f052 100644 --- a/helm/software/components/tactics/equalityTactics.ml +++ b/helm/software/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