- decompose now runs with no arguments (operates on the whole context)

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

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index c0ce1c27d359097b676a436c05923127ffc53dda..e9f530f17f49df995ae551ad5f675aef0ec25556 100644 (file)
--- 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 ->