now destruct takes an optional list of term rather than a sigle optional term

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

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 081055ce84d64ffea17c354bc635e4e091100775..a0fd3335806f1468e3c637621b4cc4f9faef0c64 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -170,8 +170,8 @@ EXTEND
        let idents = match idents with None -> [] | Some idents -> idents in
        GrafiteAst.Decompose (loc, idents)
     | IDENT "demodulate" -> GrafiteAst.Demodulate loc
-    | IDENT "destruct"; t = tactic_term ->
-        GrafiteAst.Destruct (loc, t)
+    | IDENT "destruct"; xts = OPT [ ts = tactic_term_list1 -> ts ] ->
+        GrafiteAst.Destruct (loc, xts)
     | IDENT "elim"; what = tactic_term; using = using; 
        pattern = OPT pattern_spec;
        (num, idents) = intros_spec ->
@@ -246,8 +246,6 @@ EXTEND
         GrafiteAst.Ring loc
     | IDENT "split" ->
         GrafiteAst.Split loc
-    | IDENT "subst" ->
-        GrafiteAst.Subst loc    
     | IDENT "symmetry" ->
         GrafiteAst.Symmetry loc
     | IDENT "transitivity"; t = tactic_term ->