[ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
];
reduction_kind: [
- [ IDENT "demodulate" -> `Demodulate
- | IDENT "normalize" -> `Normalize
+ [ IDENT "normalize" -> `Normalize
| IDENT "reduce" -> `Reduce
| IDENT "simplify" -> `Simpl
| IDENT "unfold"; t = OPT tactic_term -> `Unfold t
let idents = match idents with None -> [] | Some idents -> idents in
let to_spec id = GrafiteAst.Ident id in
GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents)
+ | IDENT "demodulate" -> GrafiteAst.Demodulate loc
| IDENT "discriminate"; t = tactic_term ->
GrafiteAst.Discriminate (loc, t)
| IDENT "elim"; what = tactic_term; using = using;