+ nreduction_kind: [
+ [ IDENT "nnormalize" ; delta = OPT [ IDENT "nodelta" -> () ] ->
+ let delta = match delta with None -> true | _ -> false in
+ `Normalize delta
+ (*| IDENT "unfold"; t = OPT tactic_term -> `Unfold t*)
+ | IDENT "nwhd" ; delta = OPT [ IDENT "nodelta" -> () ] ->
+ let delta = match delta with None -> true | _ -> false in
+ `Whd delta]
+ ];