new signature of auto_tac, with a new optional argument "full", to invoke the

[helm.git] / helm / matita / matitaEngine.ml

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index b065040523bc2d46d3fa2b4f3db89d91a9611ca9..4e48df8072d13a027ea5dac975936fa884d91d1f 100644 (file)
--- 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