X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=fe9ea94d66b3ba1dafab5310c035217dcb5f164a;hb=aa05519b7416dbd248f05119cce3cb4091098c7d;hp=767182bc196e60bfd635ba8f64a56e86d86f2db2;hpb=29657d5f10bd3796ba8f2cc1add48de8a02c1466;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 767182bc1..fe9ea94d6 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -59,8 +59,9 @@ let tactic_of_ast = function
   | GrafiteAst.Absurd (_, term) -> Tactics.absurd term
   | GrafiteAst.Apply (_, term) -> Tactics.apply term
   | GrafiteAst.Assumption _ -> Tactics.assumption
-  | GrafiteAst.Auto (_,depth,width) -> 
-      AutoTactic.auto_tac ?depth ?width ~dbd:(MatitaDb.instance ()) ()
+  | GrafiteAst.Auto (_,depth,width,paramodulation) -> (* ALB *)
+      AutoTactic.auto_tac ?depth ?width ?paramodulation
+        ~dbd:(MatitaDb.instance ()) ()
   | GrafiteAst.Change (_, pattern, with_what) ->
      Tactics.change ~pattern with_what
   | GrafiteAst.Clear (_,id) -> Tactics.clear id
@@ -178,7 +179,7 @@ let disambiguate_tactic status = function
       let status, cic = disambiguate_term status term in
       status, GrafiteAst.Absurd (loc, cic)
   | GrafiteAst.Assumption loc -> status, GrafiteAst.Assumption loc
-  | GrafiteAst.Auto (loc,depth,width) -> status, GrafiteAst.Auto (loc,depth,width)
+  | GrafiteAst.Auto (loc,depth,width,paramodulation) -> status, GrafiteAst.Auto (loc,depth,width,paramodulation) (* ALB *)
   | GrafiteAst.Change (loc, pattern, with_what) -> 
       let status, with_what = disambiguate_term status with_what in
       let status, pattern = disambiguate_pattern status pattern in