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 c9e46dc2af1b8523109f4b594705afb33c7435f7..daa80fd8f08690e2964db8e1469d5e21ca38f8c3 100644 (file)
--- 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