let idents = match idents with None -> [] | Some idents -> idents in
GrafiteAst.Decompose (loc, idents)
| IDENT "demodulate" -> GrafiteAst.Demodulate loc
- | IDENT "destruct"; t = tactic_term ->
- GrafiteAst.Destruct (loc, t)
+ | IDENT "destruct"; xt = OPT [ t = tactic_term -> t ] ->
+ GrafiteAst.Destruct (loc, xt)
| IDENT "elim"; what = tactic_term; using = using;
pattern = OPT pattern_spec;
(num, idents) = intros_spec ->
GrafiteAst.Ring loc
| IDENT "split" ->
GrafiteAst.Split loc
- | IDENT "subst" ->
- GrafiteAst.Subst loc
| IDENT "symmetry" ->
GrafiteAst.Symmetry loc
| IDENT "transitivity"; t = tactic_term ->