let to_spec id = GrafiteAst.Ident id in
GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents)
| IDENT "demodulate" -> GrafiteAst.Demodulate loc
- | IDENT "discriminate"; t = tactic_term ->
- GrafiteAst.Discriminate (loc, t)
+ | IDENT "destruct"; t = tactic_term ->
+ GrafiteAst.Destruct (loc, t)
| IDENT "elim"; what = tactic_term; using = using;
(num, idents) = intros_spec ->
GrafiteAst.Elim (loc, what, using, num, idents)
| IDENT "goal"; n = int ->
GrafiteAst.Goal (loc, n)
| IDENT "id" -> GrafiteAst.IdTac loc
- | IDENT "injection"; t = tactic_term ->
- GrafiteAst.Injection (loc, t)
| IDENT "intro"; ident = OPT IDENT ->
let idents = match ident with None -> [] | Some id -> [id] in
GrafiteAst.Intros (loc, Some 1, idents)