| LetIn of name * what * note
| Rewrite of how * what * where * pattern * note
| Elim of what * using option * pattern * note
+ | Cases of what * pattern * note
| Apply of what * note
| Change of inferred * what * where * pattern * note
| Clear of hyp list * note
let tactic = G.Elim (floc, what, using, pattern, (Some 0, [])) in
mk_tactic tactic punctation
+let mk_cases what pattern punctation =
+ let pattern = None, [], Some pattern in
+ let tactic = G.Cases (floc, what, pattern, (Some 0, [])) in
+ mk_tactic tactic punctation
+
let mk_apply t punctation =
let tactic = G.ApplyP (floc, t) in
mk_tactic tactic punctation
| LetIn (n, t, s) -> mk_letin n t sep :: mk_tacnote s a
| Rewrite (b, t, w, e, s) -> mk_rewrite b t w e sep :: mk_tacnote s a
| Elim (t, xu, e, s) -> mk_elim t xu e sep :: mk_tacnote s a
+ | Cases (t, e, s) -> mk_cases t e sep :: mk_tacnote s a
| Apply (t, s) -> mk_apply t sep :: mk_tacnote s a
| Change (t, _, w, e, s) -> mk_change t w e sep :: mk_tacnote s a
| Clear (ns, s) -> mk_clear ns sep :: mk_tacnote s a
| Apply (t, _) -> I.count_nodes a (H.cic t)
| Rewrite (_, t, _, p, _)
| Elim (t, _, p, _)
+ | Cases (t, p, _)
| Change (t, _, _, p, _) ->
let a = I.count_nodes a (H.cic t) in
I.count_nodes a (H.cic p)