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