- init_cache_and_tables rewritten using the automation_cache

[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 2a5d3c0b0777fe500bef007004befa0e436167c4..b6930bf0df234357e2a4e5f51e673d892726e204 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -743,6 +743,8 @@ EXTEND
          (loc, t, composites, arity, saturations)
     | IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
         GrafiteAst.PreferCoercion (loc, t)
+    | IDENT "pump" ; steps = int ->
+        GrafiteAst.Pump(loc,steps)
     | IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
         GrafiteAst.UnificationHint (loc, t, n)
     | IDENT "record" ; (params,name,ty,fields) = record_spec ->