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=c0ce1c27d359097b676a436c05923127ffc53dda;hpb=3b7bfb05e6fc1a2ac6864d8f7d959fcda0597d21;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index c0ce1c27d..e9f530f17 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -136,8 +136,8 @@ EXTEND
         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"; id = IDENT ->
-        GrafiteAst.Clear (loc,id)
+    | 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 ->
@@ -148,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 ->