principles = ident_list1; where = IDENT ->
TacticAst.Decompose (loc, where, principles)
| [ IDENT "discriminate" ];
- hyp = IDENT ->
- TacticAst.Discriminate (loc, hyp)
+ t = tactic_term ->
+ TacticAst.Discriminate (loc, t)
| [ IDENT "elimType" ]; t = tactic_term ->
TacticAst.ElimType (loc, t)
| [ IDENT "elim" ];