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