added optional "paramodulation" parameter to auto to turn on paramodulation

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index d0223a80bccf8e0b7f7cb1ff8a7bb430dcf95051..d4f9c3fac85bd102e472bc2a9e06648b20b65e4a 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -31,7 +31,7 @@ open MatitaMisc
 
 
 (* ALB to link paramodulation... *)
-let _ = Saturation.init ()
+let _ = Paramodulation.Saturation.init ()
   
 
 (** {2 Initialization} *)

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 767182bc196e60bfd635ba8f64a56e86d86f2db2..fe9ea94d66b3ba1dafab5310c035217dcb5f164a 100644 (file)
--- 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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 108b36bfb3f8738ac008a02f65bf1e7207488ef6..d21241a8dd4bc3c84afcb958b440454221a47196 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -524,7 +524,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)));
+      connect_button tbar#autoButton (tac (A.Auto (loc,None,None,None))); (* ALB *)
       MatitaGtkMisc.toggle_widget_visibility
        ~widget:(self#main#tacticsButtonsHandlebox :> GObj.widget)
        ~check:self#main#tacticsBarMenuItem;

diff --git a/helm/matita/matitac.ml b/helm/matita/matitac.ml
index b27e115f43f86e27c6dc637196b0331d6c4b7e59..40526e74d4a4a59eed02f77f14bc5492ee526ddd 100644 (file)
--- a/helm/matita/matitac.ml
+++ b/helm/matita/matitac.ml
@@ -25,7 +25,7 @@
 
 
 (* ALB to link paramodulation... *)
-let _ = Saturation.init ()
+let _ = Paramodulation.Saturation.init ()
 
   
 let _ = MatitacLib.main `COMPILER

diff --git a/helm/matita/tests/paramodulation.ma b/helm/matita/tests/paramodulation.ma
index af8d59be6d053b60e424a675824d07f942c60399..b56c0da27d1672cf11046bb0bee882048c8997b3 100644 (file)
--- a/helm/matita/tests/paramodulation.ma
+++ b/helm/matita/tests/paramodulation.ma
@@ -22,10 +22,10 @@ alias symbol "times" (instance 0) = "natural times".
 theorem para1:
   \forall n,m,n1,m1:nat.
     n=m \to n1 = m1 \to (n + n1) = (m + m1).
-intros. auto.
+intros. auto paramodulation.
 qed.
 
 theorem para2:
   \forall n:nat. n + n = 2 * n.
-intros. auto.
-qed.
\ No newline at end of file
+intros. auto paramodulation.
+qed.