GrafiteAst.NChange (loc, what, with_what)
| IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
GrafiteAst.NElim (loc, what, where)
+ | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->
+ GrafiteAst.NRewrite (loc, dir, what, where)
| SYMBOL "#"; n=IDENT -> GrafiteAst.NIntro (loc,n)
| SYMBOL "#"; SYMBOL "_" -> GrafiteAst.NIntro (loc,"_")
| SYMBOL "*" -> GrafiteAst.NCase1 (loc,"_")