[ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
];
reduction_kind: [
- [ IDENT "reduce" -> `Reduce
+ [ IDENT "normalize" -> `Normalize
+ | IDENT "reduce" -> `Reduce
| IDENT "simplify" -> `Simpl
- | IDENT "whd" -> `Whd
- | IDENT "normalize" -> `Normalize ]
+ | IDENT "unfold"; t = OPT term -> `Unfold t
+ | IDENT "whd" -> `Whd ]
];
sequent_pattern_spec: [
[ hyp_paths =