From 17e81891da2a278891276e923d479e3834e22c07 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 31 Mar 2010 14:41:09 +0000 Subject: [PATCH] Bug fixed: the current equation is not always the last hyp. From: sacerdot --- helm/software/components/ng_tactics/nDestructTac.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/ng_tactics/nDestructTac.ml b/helm/software/components/ng_tactics/nDestructTac.ml index 103791c03..3a8e257f9 100644 --- a/helm/software/components/ng_tactics/nDestructTac.ml +++ b/helm/software/components/ng_tactics/nDestructTac.ml @@ -366,7 +366,7 @@ let subst_tac ~context ~dir cur_eq = | _ -> assert false in let names_to_gen, _ = cascade_select_in_ctx ~subst:(get_subst status) context (var+cur_eq) in - let names_to_gen = match names_to_gen with [] -> [] | _::tl -> tl in + let names_to_gen = List.filter (fun n -> n <> eq_name) names_to_gen in let gen_tac x = NTactics.generalize_tac ~where:("",0,(Some (mk_id x),[], Some CicNotationPt.UserInput)) in -- 2.39.2