X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteEngine.ml;h=ae497fc12cbdd25db29b319643cfbe444d421aa0;hb=3eec3be7243166d6a157a8e4e914cd4076c813e3;hp=ff173bc37aa1d717ed3b7e32f69d26043b5a9b42;hpb=1b3f24947f19050f3947397e50a8d5ed3b61b71b;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index ff173bc37..ae497fc12 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -60,10 +60,11 @@ 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
-        ~dbd:(LibraryDb.instance ()) ()
+  | GrafiteAst.Auto (_,params) ->
+      AutoTactic.auto_tac ~params ~dbd:(LibraryDb.instance ()) 
   | GrafiteAst.Change (_, pattern, with_what) ->
      Tactics.change ~pattern with_what
   | GrafiteAst.Clear (_,id) -> Tactics.clear id