X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=2316c04cad0bb9934d47514e917bf0b5ed643a12;hb=d58b48162ad53fb369d285e60a99f746a497ad89;hp=8f37c918e83e8834446ddc667cb835dfc95bb04f;hpb=6ec246c70b05bb310ee5364c3774ea69b0fc9e57;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 8f37c918e..2316c04ca 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -188,6 +188,8 @@ EXTEND
         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,"_")