From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 24 Nov 2011 22:34:36 +0000 (+0000)
Subject: Destruct: we warn about the substituted variable to remove.
X-Git-Tag: make_still_working~2062
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3c2b1af52212c320f6e4506d10df7077379a222c;p=helm.git

Destruct: we warn about the substituted variable to remove.
In this way, now we know that this is the wrong variable sometimes
(esp. when the equations are more than one).
A bugfix will follow
---

diff --git a/matita/components/ng_tactics/nDestructTac.ml b/matita/components/ng_tactics/nDestructTac.ml
index c9e46dc2a..daa80fd8f 100644
--- a/matita/components/ng_tactics/nDestructTac.ml
+++ b/matita/components/ng_tactics/nDestructTac.ml
@@ -471,7 +471,9 @@ 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 [name]
+          let name,_ = List.nth context var in
+	  HLog.warn (Printf.sprintf "destruct: trying to remove variable: %s" name);
+	  [name]
       | _ -> []
     in      
     let names_to_gen = List.filter (fun n -> n <> eq_name) names_to_gen in