- 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
+ 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_eq");
+ NTactics.shift_tac;
+ (*NTactics.case_tac "cut";*)
+ NTactics.apply_tac ("",0,t);
+ NTactics.merge_tac;
+ NTactics.merge_tac;
+ NTactics.skip_tac])) status in