| IDENT "demodulate" -> GrafiteAst.Demodulate loc
| IDENT "destruct"; t = tactic_term ->
GrafiteAst.Destruct (loc, t)
- | IDENT "elim"; what = tactic_term; using = using;
+ | IDENT "elim"; what = tactic_term; using = using;
+ pattern = OPT pattern_spec;
(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, pattern, using, num, idents)
+ let pattern = match pattern with
+ | None -> None, [], Some Ast.UserInput
+ | Some pattern -> pattern
+ in
+ GrafiteAst.Elim (loc, what, using, pattern, num, idents)
| IDENT "elimType"; what = tactic_term; using = using;
(num, idents) = intros_spec ->
GrafiteAst.ElimType (loc, what, using, num, idents)