X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_parser%2FgrafiteParser.ml;h=2d37892217407440aac8957ee8c9029ff1bc9613;hb=2e3e85acace6942eebcfac570ce6b33134d1a3dd;hp=586cca004a50f1563bca7e6a3857d160a025082b;hpb=5cd2bfac5e47232f9e1a8f6189bcc49a3e73007f;p=helm.git

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 586cca004..2d3789221 100644
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -218,8 +218,6 @@ 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;
@@ -428,11 +426,11 @@ EXTEND
     [ [ IDENT "check"   ]; t = term ->
         GrafiteAst.Check (loc, t)
     | [ IDENT "inline"]; 
-        style = OPT [ IDENT "procedural" ];
+        style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
 	suri = QSTRING; prefix = OPT QSTRING ->
          let style = match style with 
-	    | None   -> GrafiteAst.Declarative
-	    | Some _ -> GrafiteAst.Procedural
+	    | None       -> GrafiteAst.Declarative
+	    | Some depth -> GrafiteAst.Procedural depth
 	 in
 	 let prefix = match prefix with None -> "" | Some prefix -> prefix in
 	 GrafiteAst.Inline (loc,style,suri,prefix)