From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 10 Mar 2007 22:23:38 +0000 (+0000)
Subject: rewrite tactic: bug fix in rewriting under Pi's:
X-Git-Tag: 0.4.95@7852~572
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5813d9a88f34f0c0d15cb74243f638d02ae163fa;p=helm.git

rewrite tactic: bug fix in rewriting under Pi's:
                the application context of the subterm to rewrite can not be
		forgotten
---

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