- let status = NTactics.block_tac
- (NTactics.branch_tac ::
- NTactics.case_tac "inv" ::
- (intros @
- [NTactics.apply_tac ("",0,cut);
- NTactics.branch_tac;
- NTactics.case_tac "end";
- NTactics.apply_tac ("",0,mk_id "Hcut");
- NTactics.apply_tac ("",0,mk_id "refl");
- NTactics.shift_tac;
- (*NTactics.case_tac "cut";*)
- NTactics.apply_tac ("",0,t);
- NTactics.merge_tac;
- NTactics.merge_tac;
- NTactics.skip_tac])) status in
+ let where =
+ "",0,(None,[],
+ Some (
+ mk_arrows ~pattern:true
+ (HExtlib.mk_list (CicNotationPt.Implicit `JustOne) (List.length ys))
+ (HExtlib.mk_list CicNotationPt.UserInput (List.length ys))
+ selection CicNotationPt.UserInput)) in
+ let elim_tac = if is_ind then NTactics.elim_tac else NTactics.cases_tac in
+ let status =
+ NTactics.block_tac
+ (NTactics.branch_tac ::
+ NTactics.case_tac "inv" ::
+ (intros @
+ [NTactics.apply_tac ("",0,cut);
+ NTactics.branch_tac;
+ NTactics.case_tac "end";
+ NTactics.apply_tac ("",0,mk_id "Hcut");
+ NTactics.apply_tac ("",0,mk_id "refl");
+ NTactics.shift_tac;
+ elim_tac ~what:("",0,mk_id "Hterm") ~where;
+ NTactics.branch_tac ~force:true] @
+ HExtlib.list_concat ~sep:[NTactics.shift_tac]
+ (List.map (fun id-> [NTactics.apply_tac ("",0,mk_id id)]) hyplist) @
+ [NTactics.merge_tac;
+ NTactics.merge_tac;
+ NTactics.merge_tac;
+ NTactics.skip_tac])) status in