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

new paramodulation

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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 5d223208f042f782ee409e890272a15cef3e2441..8351426f88702e4191141634596cafd1c2323c6a 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -549,7 +549,7 @@ class gui () =
         (tac_w_term (A.Transitivity (loc, hole)));
       connect_button tbar#assumptionButton (tac (A.Assumption loc));
       connect_button tbar#cutButton (tac_w_term (A.Cut (loc, None, hole)));
-      connect_button tbar#autoButton (tac (A.Auto (loc,None,None,None)));
+      connect_button tbar#autoButton (tac (A.Auto (loc,None,None,None,None)));
       MatitaGtkMisc.toggle_widget_visibility
        ~widget:(main#tacticsButtonsHandlebox :> GObj.widget)
        ~check:main#tacticsBarMenuItem;