* http://helm.cs.unibo.it/
*)
+(* $Id$ *)
+
open Printf
module Ast = CicNotationPt
[ tactic_terms = LIST1 tactic_term SEP SYMBOL "," -> tactic_terms ]
];
reduction_kind: [
- [ IDENT "normalize" -> `Normalize
+ [ IDENT "demodulate" -> `Demodulate
+ | IDENT "normalize" -> `Normalize
| IDENT "reduce" -> `Reduce
| IDENT "simplify" -> `Simpl
| IDENT "unfold"; t = OPT term -> `Unfold t