mk_tactic tactic punctation
let mk_apply t punctation =
- let tactic = G.ApplyP (floc, t) in
+ let tactic = G.Apply (floc, t) in
mk_tactic tactic punctation
let mk_change t where pattern punctation =
let rec count_step a = function
| Note _
- | Statement _
+ | Statement _
+ | Inductive _
+ | Qed _
+(* level 0 *)
+ | Intros (Some 0, [], _)
| Id _
| Exact _
- | Qed _ -> a
- | Branch (pps, _) -> List.fold_left count_steps a pps
- | _ -> succ a
+ | Change _
+ | Clear _
+ | ClearBody _ -> a
+ | Branch (pps, _) -> List.fold_left count_steps a pps
+(* level 1 *)
+ | _ -> succ a
and count_steps a = List.fold_left count_step a
| Note _
| Inductive _
| Statement _
- | Qed _
+ | Qed _
| Id _
| Intros _
| Clear _