added (but not yet used) remove_local_context

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

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 5bf73503b7503677b49341dae3956c7e58d84399..cbaed19b099d148a85805b75745fc4675e9297cc 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -128,6 +128,8 @@ EXTEND
         GrafiteAst.Absurd (loc, t)
     | IDENT "apply"; t = tactic_term ->
         GrafiteAst.Apply (loc, t)
+    | IDENT "applyS"; t = tactic_term ->
+        GrafiteAst.ApplyS (loc, t)
     | IDENT "assumption" ->
         GrafiteAst.Assumption loc
     | IDENT "auto";