| IDENT "destruct"; t = tactic_term ->
GrafiteAst.Destruct (loc, t)
| IDENT "elim"; what = tactic_term; using = using;
+ (num, idents) = intros_spec ->
+ let pattern = Some what, [], Some Ast.UserInput in
+ GrafiteAst.Elim (loc, pattern, using, num, idents)
+ | IDENT "elim"; pattern = pattern_spec; using = using;
(num, idents) = intros_spec ->
- GrafiteAst.Elim (loc, what, using, num, idents)
+ GrafiteAst.Elim (loc, pattern, using, num, idents)
| IDENT "elimType"; what = tactic_term; using = using;
(num, idents) = intros_spec ->
GrafiteAst.ElimType (loc, what, using, num, idents)