]> matita.cs.unibo.it Git - helm.git/commitdiff
rewrite tactic: bug fix in rewriting under Pi's:
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 10 Mar 2007 22:23:38 +0000 (22:23 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Sat, 10 Mar 2007 22:23:38 +0000 (22:23 +0000)
                the application context of the subterm to rewrite can not be
forgotten

helm/software/components/tactics/equalityTactics.ml

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