X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_parser%2FgrafiteParser.ml;h=c4e12ac080a18a1786c7efbf9cdd9a0dab9a9a40;hb=e9ffdf3ca123648c696ec331ba5ac031ca900480;hp=5f256a1e06864d2e022a126592e7848b324ab843;hpb=27ebdab06ba308c431669b58a46fc0bb12c8c72e;p=helm.git

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 5f256a1e0..c4e12ac08 100644
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -233,6 +233,8 @@ EXTEND
         GrafiteAst.Ring loc
     | IDENT "split" ->
         GrafiteAst.Split loc
+    | IDENT "subst" ->
+        GrafiteAst.Subst loc    
     | IDENT "symmetry" ->
         GrafiteAst.Symmetry loc
     | IDENT "transitivity"; t = tactic_term ->
@@ -325,6 +327,7 @@ EXTEND
       | IDENT "solve";
         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
           GrafiteAst.Solve (loc, tacs)
+      | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
       | LPAREN; tac = SELF; RPAREN -> tac
       | tac = tactic -> GrafiteAst.Tactic (loc, tac)
       ]