| IDENT "unfold"; t = OPT tactic_term -> `Unfold t
| IDENT "whd" -> `Whd ]
];
+ 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]
+ ];
sequent_pattern_spec: [
[ hyp_paths =
LIST0
| IDENT "nletin"; name = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term;
where = pattern_spec ->
G.NLetIn (loc,where,t,name)
+ | kind = nreduction_kind; p = pattern_spec ->
+ G.NReduce (loc, kind, p)
| IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
G.NRewrite (loc, dir, what, where)
- | IDENT "nwhd"; delta = OPT [ IDENT "nodelta" -> () ];
- where = pattern_spec ->
- let delta = match delta with None -> true | _ -> false in
- G.NEval (loc, where, `Whd delta)
| SYMBOL "#"; n=IDENT -> G.NIntro (loc,n)
| SYMBOL "#"; SYMBOL "_" -> G.NIntro (loc,"_")
| SYMBOL "*" -> G.NCase1 (loc,"_")
G.NTactic (loc, G.NId loc, punct)
| tac = non_punctuation_tactical; punct = punctuation_tactical ->
G.NonPunctuationTactical (loc, tac, punct)
+ | SYMBOL "#" ; SYMBOL "#" ; tac = non_punctuation_tactical; punct = punctuation_tactical ->
+ G.NNonPunctuationTactical (loc, tac, punct)
| mac = macro; SYMBOL "." -> G.Macro (loc, mac)
]
];