X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_parser%2FgrafiteParser.ml;h=83e9d10d879904456952cfacf10bb03f60becd69;hb=ef870606391fff198f215127eb022eb3e41ab1d4;hp=081055ce84d64ffea17c354bc635e4e091100775;hpb=040b70279b9bf0f576f00a9b1ad28df3c8bf6024;p=helm.git

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 081055ce8..83e9d10d8 100644
--- 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"; xt = OPT [ t = tactic_term -> t ] ->
+        GrafiteAst.Destruct (loc, xt)
     | 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 ->