auto and autogui... some work

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

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 05504f511f3c149913256f7740cffb861b231730..17144a85244a40cea868499ac3ce36c1fb535059 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -145,8 +145,8 @@ EXTEND
         GrafiteAst.ApplyS (loc, t, params)
     | IDENT "assumption" ->
         GrafiteAst.Assumption loc
-    | IDENT "auto"; params = auto_params ->
-        GrafiteAst.Auto (loc,params)
+    | IDENT "autobatch";  params = auto_params ->
+        GrafiteAst.AutoBatch (loc,params)
     | IDENT "cases"; what = tactic_term;
       specs = intros_spec ->
        GrafiteAst.Cases (loc, what, specs)
@@ -439,6 +439,8 @@ EXTEND
         let prefix = match prefix with None -> "" | Some prefix -> prefix in
         GrafiteAst.Inline (loc,style,suri,prefix)
     | [ IDENT "hint" ] -> GrafiteAst.Hint loc
+    | IDENT "auto"; params = auto_params ->
+        GrafiteAst.AutoInteractive (loc,params)
     | [ IDENT "whelp"; "match" ] ; t = term -> 
         GrafiteAst.WMatch (loc,t)
     | [ IDENT "whelp"; IDENT "instance" ] ; t = term ->