X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_parser%2FgrafiteParser.ml;h=10a841e2eae14e01db81a03147ca3ace7ebb8bfe;hb=614e3c3fb219e404e60810bfc04072351803b8e8;hp=05504f511f3c149913256f7740cffb861b231730;hpb=b8254cf86275b9d78b30a0b14974a6f23ad9be24;p=helm.git

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 05504f511..10a841e2e 100644
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -145,17 +145,20 @@ 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)
+        GrafiteAst.Cases (loc, what, specs)
     | IDENT "clear"; ids = LIST1 IDENT ->
         GrafiteAst.Clear (loc, ids)
     | IDENT "clearbody"; id = IDENT ->
         GrafiteAst.ClearBody (loc,id)
     | IDENT "change"; what = pattern_spec; "with"; t = tactic_term ->
         GrafiteAst.Change (loc, what, t)
+    | IDENT "compose"; t1 = tactic_term; t2 = tactic_term;
+      specs = intros_spec ->
+        GrafiteAst.Compose (loc, t1, t2, specs)
     | IDENT "constructor"; n = int ->
         GrafiteAst.Constructor (loc, n)
     | IDENT "contradiction" ->
@@ -439,6 +442,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 ->