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 ->
+ | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
G.NRewrite (loc, dir, what, where)
+ | IDENT "ntry"; LPAREN ; tac = SELF ; RPAREN -> G.NTry (loc,tac)
+ | IDENT "nassumption" -> G.NAssumption loc
| SYMBOL "#"; n=IDENT -> G.NIntro (loc,n)
| SYMBOL "#"; SYMBOL "_" -> G.NIntro (loc,"_")
| SYMBOL "*" -> G.NCase1 (loc,"_")