From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 25 Nov 2011 15:24:29 +0000 (+0000)
Subject: bugfix in clearing the replaced variable: a relocation was missing
X-Git-Tag: make_still_working~2061
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2b5892c042136ebb0d9a2f773f3174c840ca0ba6;p=helm.git

bugfix in clearing the replaced variable: a relocation was missing
---

diff --git a/matita/components/ng_tactics/nDestructTac.ml b/matita/components/ng_tactics/nDestructTac.ml
index daa80fd8f..be9914840 100644
--- a/matita/components/ng_tactics/nDestructTac.ml
+++ b/matita/components/ng_tactics/nDestructTac.ml
@@ -471,7 +471,7 @@ let subst_tac ~context ~dir skip cur_eq =
       | _ -> cascade_select_in_ctx status ~subst:(get_subst status) context skip cur_eq in
     let varname = match var with
       | NCic.Rel var -> 
-          let name,_ = List.nth context var in
+          let name,_ = List.nth context (var+cur_eq-1) in
 	  HLog.warn (Printf.sprintf "destruct: trying to remove variable: %s" name);
 	  [name]
       | _ -> []
@@ -497,7 +497,7 @@ let subst_tac ~context ~dir skip cur_eq =
                  (* XXX: temo che la clear multipla funzioni bene soltanto se
                   * gli identificatori sono nell'ordine giusto.
                   * Per non saper né leggere né scrivere, usiamo due clear
-                  * invece di una *)		   
+                  * invece di una *)
                  NTactics.try_tac (NTactics.clear_tac [eq_name]);
 		 NTactics.try_tac (NTactics.clear_tac varname);
 ]@