Apply-Silvie tactic added!

[helm.git] / components / grafite_engine / grafiteEngine.ml

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index ff173bc37aa1d717ed3b7e32f69d26043b5a9b42..e4f70117a344bb41db8700aaa5d588d2cd3b834c 100644 (file)
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/components/grafite_engine/grafiteEngine.ml
@@ -60,6 +60,8 @@ let tactic_of_ast ast =
   match ast with
   | GrafiteAst.Absurd (_, term) -> Tactics.absurd term
   | GrafiteAst.Apply (_, term) -> Tactics.apply term
+  | GrafiteAst.ApplyS (_, term) ->
+     Tactics.applyS ~term ~dbd:(LibraryDb.instance ())
   | GrafiteAst.Assumption _ -> Tactics.assumption
   | GrafiteAst.Auto (_,depth,width,paramodulation,full) ->
       AutoTactic.auto_tac ?depth ?width ?paramodulation ?full