TacticAst.Decompose (loc, where)
| IDENT "discriminate"; t = tactic_term ->
TacticAst.Discriminate (loc, t)
- | IDENT "elim"; t1 = tactic_term;
- using = OPT [ "using"; using = tactic_term -> using ] ->
- TacticAst.Elim (loc, t1, using)
- | IDENT "elimType"; t = tactic_term ->
- TacticAst.ElimType (loc, t)
+ | IDENT "elim"; what = tactic_term;
+ using = OPT [ "using"; using = tactic_term -> using ];
+ OPT "names"; num = OPT [num = int -> num]; idents = OPT ident_list0 ->
+ let idents = match idents with None -> [] | Some idents -> idents in
+ TacticAst.Elim (loc, what, using, num, idents)
+ | IDENT "elimType"; what = tactic_term;
+ using = OPT [ "using"; using = tactic_term -> using ];
+ OPT "names"; num = OPT [num = int -> num]; idents = OPT ident_list0 ->
+ let idents = match idents with None -> [] | Some idents -> idents in
+ TacticAst.ElimType (loc, what, using, num, idents)
| IDENT "exact"; t = tactic_term ->
TacticAst.Exact (loc, t)
| IDENT "exists" ->