From 3c2b1af52212c320f6e4506d10df7077379a222c Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 24 Nov 2011 22:34:36 +0000 Subject: [PATCH] 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 --- matita/components/ng_tactics/nDestructTac.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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 -- 2.39.2