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: make_still_working~6431
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=5cf27f4cc19d59ed91cda9d8ec7d702c32384378;hp=c0a733b932a64804f67ac93f9ab9f52bd0614fc6;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/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