- | [ IDENT "cut" ];
- t = tactic_term ->
- TacticAst.Cut (loc, t)
- | [ IDENT "decompose" ];
- principles = ident_list1; where = IDENT ->
- TacticAst.Decompose (loc, where, principles)
- | [ IDENT "discriminate" ];
- hyp = IDENT ->
- TacticAst.Discriminate (loc, hyp)
- | [ IDENT "elimType" ]; t = tactic_term ->
- TacticAst.ElimType (loc, t)
- | [ IDENT "elim" ];
- t1 = tactic_term;
- using = OPT [ "using"; using = tactic_term -> using ] ->
- TacticAst.Elim (loc, t1, using)
- | [ IDENT "exact" ]; t = tactic_term ->
+ | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
+ TacticAst.Cut (loc, ident, t)
+ | IDENT "decide"; IDENT "equality" ->
+ TacticAst.DecideEquality loc
+ | IDENT "decompose"; where = tactic_term ->
+ TacticAst.Decompose (loc, where)
+ | IDENT "discriminate"; t = tactic_term ->
+ TacticAst.Discriminate (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 ->