leftno m))
(nbranches-1) [] in
if nbranches > 1 then
- NTactics.branch_tac:: branches @ [NTactics.merge_tac]
+ NTactics.branch_tac ~force:false:: branches @ [NTactics.merge_tac]
else branches
in
| _ -> 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