X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=e9f530f17f49df995ae551ad5f675aef0ec25556;hb=cc3ab906b631ef0edb4402cb622fc3fa96682717;hp=535e396a9324703959145a1e97b662ce9fc287e8;hpb=0fe1347ecafd65a4be26f85595032653f81d1ab3;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 535e396a9..e9f530f17 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -132,14 +132,12 @@ EXTEND
         GrafiteAst.ApplyS (loc, t)
     | IDENT "assumption" ->
         GrafiteAst.Assumption loc
-    | IDENT "auto";
-      depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
-      width = OPT [ IDENT "width"; SYMBOL "="; i = int -> i ];
-      paramodulation = OPT [ IDENT "paramodulation" ];
-      full = OPT [ IDENT "full" ] ->  (* ALB *)
-          GrafiteAst.Auto (loc,depth,width,paramodulation,full)
-    | IDENT "clear"; id = IDENT ->
-        GrafiteAst.Clear (loc,id)
+    | IDENT "auto"; params = 
+        LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
+          string_of_int v | v = IDENT -> v ] -> i,v ] ->
+        GrafiteAst.Auto (loc,params)
+    | 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 ->
@@ -150,9 +148,10 @@ EXTEND
         GrafiteAst.Contradiction loc
     | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] ->
         GrafiteAst.Cut (loc, ident, t)
-    | IDENT "decompose"; types = OPT ident_list0; what = IDENT;
-      (num, idents) = intros_spec ->
+    | IDENT "decompose"; types = OPT ident_list0; what = OPT IDENT;
+        idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
         let types = match types with None -> [] | Some types -> types in
+	let idents = match idents with None -> [] | Some idents -> idents in
 	let to_spec id = GrafiteAst.Ident id in
 	GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents)
     | IDENT "discriminate"; t = tactic_term ->
@@ -178,7 +177,7 @@ EXTEND
          GrafiteAst.Fold (loc, kind, t, p)
     | IDENT "fourier" ->
         GrafiteAst.Fourier loc
-    | IDENT "fwd"; hyp = IDENT; idents = OPT ident_list0 ->
+    | IDENT "fwd"; hyp = IDENT; idents = OPT [ "as"; idents = LIST1 IDENT -> idents ] ->
         let idents = match idents with None -> [] | Some idents -> idents in
         GrafiteAst.FwdSimpl (loc, hyp, idents)
     | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->