matitaGui: some missing cases during disambiguation now treated

[helm.git] / components / grafite_parser / grafiteParser.ml

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 586cca004a50f1563bca7e6a3857d160a025082b..2d37892217407440aac8957ee8c9029ff1bc9613 100644 (file)
--- 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)