X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_parser%2FgrafiteParser.ml;h=586cca004a50f1563bca7e6a3857d160a025082b;hb=3f586b01da59fe16b3d7f37da28bdd71f2225131;hp=054bff6215e1f64ec1b6d90813a3f7a316b88089;hpb=172588c02ff4d9ed5cc03265c2bd6a36f8a0f5da;p=helm.git

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 054bff621..586cca004 100644
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -218,9 +218,12 @@ EXTEND
         GrafiteAst.Reduce (loc, kind, p)
     | IDENT "reflexivity" ->
         GrafiteAst.Reflexivity loc
+    | IDENT "rename"; froms = ident_list0; "as"; tos = ident_list0 ->
+	GrafiteAst.Rename (loc, froms, tos)
     | IDENT "replace"; p = pattern_spec; "with"; t = tactic_term ->
         GrafiteAst.Replace (loc, p, t)
-    | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec ->
+    | IDENT "rewrite" ; d = direction; t = tactic_term ; p = pattern_spec;
+       xnames = OPT [ "as"; n = ident_list0 -> n ] ->
        let (pt,_,_) = p in
         if pt <> None then
          raise
@@ -228,7 +231,8 @@ EXTEND
            (CicNotationParser.Parse_error
             "the pattern cannot specify the term to rewrite, only its paths in the hypotheses and in the conclusion")))
         else
-         GrafiteAst.Rewrite (loc, d, t, p)
+	 let n = match xnames with None -> [] | Some names -> names in 
+         GrafiteAst.Rewrite (loc, d, t, p, n)
     | IDENT "right" ->
         GrafiteAst.Right loc
     | IDENT "ring" ->