added the geniric

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

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index e4f70117a344bb41db8700aaa5d588d2cd3b834c..ae497fc12cbdd25db29b319643cfbe444d421aa0 100644 (file)
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/components/grafite_engine/grafiteEngine.ml
@@ -63,9 +63,8 @@ let tactic_of_ast ast =
   | 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