X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=4e48df8072d13a027ea5dac975936fa884d91d1f;hb=0a17483072707b5a460a6c04571c6ddfc5875ce2;hp=b065040523bc2d46d3fa2b4f3db89d91a9611ca9;hpb=b2f2e47efe1e01df81cb7659c30eeb76f1f830da;p=helm.git

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index b06504052..4e48df807 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -65,8 +65,8 @@ let tactic_of_ast ast =
   | GrafiteAst.Absurd (_, term) -> Tactics.absurd term
   | GrafiteAst.Apply (_, term) -> Tactics.apply term
   | GrafiteAst.Assumption _ -> Tactics.assumption
-  | GrafiteAst.Auto (_,depth,width,paramodulation) ->
-      AutoTactic.auto_tac ?depth ?width ?paramodulation
+  | GrafiteAst.Auto (_,depth,width,paramodulation,full) ->
+      AutoTactic.auto_tac ?depth ?width ?paramodulation ?full
         ~dbd:(MatitaDb.instance ()) ()
   | GrafiteAst.Change (_, pattern, with_what) ->
      Tactics.change ~pattern with_what
@@ -227,8 +227,8 @@ let disambiguate_tactic status tactic =
         let cic = disambiguate_term status_ref term in
         GrafiteAst.Apply (loc, cic)
     | GrafiteAst.Assumption loc -> GrafiteAst.Assumption loc
-    | GrafiteAst.Auto (loc,depth,width,paramodulation) ->
-        GrafiteAst.Auto (loc,depth,width,paramodulation)
+    | GrafiteAst.Auto (loc,depth,width,paramodulation,full) ->
+        GrafiteAst.Auto (loc,depth,width,paramodulation,full)
     | GrafiteAst.Change (loc, pattern, with_what) -> 
         let with_what = disambiguate_lazy_term status_ref with_what in
         let pattern = disambiguate_pattern status_ref pattern in