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 b445dfb868d8d354aeaafb6ad303c43830de5865..a31b0f052817fb60dc14ff1fb2d9cb1d71b13365 100644 (file)
--- 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