| "whd" -> `Whd ]
];
tactic: [
- [ [ IDENT "absurd" | IDENT "Absurd" ] -> return_tactic loc TacticAst.Absurd
- | [ IDENT "apply" | IDENT "Apply" ];
- t = tactic_term -> return_tactic loc (TacticAst.Apply t)
+ [ [ IDENT "absurd" | IDENT "Absurd" ]; t = tactic_term ->
+ return_tactic loc (TacticAst.Absurd t)
+ | [ IDENT "apply" | IDENT "Apply" ]; t = tactic_term ->
+ return_tactic loc (TacticAst.Apply t)
| [ IDENT "assumption" | IDENT "Assumption" ] ->
return_tactic loc TacticAst.Assumption
| [ IDENT "change" | IDENT "Change" ];
| [ IDENT "discriminate" | IDENT "Discriminate" ];
hyp = IDENT ->
return_tactic loc (TacticAst.Discriminate hyp)
- | [ IDENT "elim" | IDENT "Elim" ]; IDENT "type";
- t = tactic_term ->
+ | [ IDENT "elimType" | IDENT "ElimType" ]; t = tactic_term ->
return_tactic loc (TacticAst.ElimType t)
| [ IDENT "elim" | IDENT "Elim" ];
t1 = tactic_term;
return_command loc (TacticAst.Undo (int_opt steps))
| [ IDENT "redo" | IDENT "Redo" ]; steps = OPT NUM ->
return_command loc (TacticAst.Redo (int_opt steps))
+ | [ IDENT "check" | IDENT "Check" ]; t = term ->
+ return_command loc (TacticAst.Check t)
]
];
END