X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FautoTactic.ml;h=cdfcf8c73ec560dfaf887bb9540e0267e4503659;hb=2e4a77477a9b809d9c1197e0693d2cdd43258570;hp=25696d7945448532efe981a56979a6bb61398320;hpb=46834f1afe49d481045a40fb1bf6ddbddcfef9f5;p=helm.git

diff --git a/helm/software/components/tactics/autoTactic.ml b/helm/software/components/tactics/autoTactic.ml
index 25696d794..cdfcf8c73 100644
--- a/helm/software/components/tactics/autoTactic.ml
+++ b/helm/software/components/tactics/autoTactic.ml
@@ -322,6 +322,8 @@ let auto_tac ~params ~(dbd:HMysql.dbd) (proof, goal) =
   let int = int params in
   let bool = bool params in
   let newauto = bool "new" false in
+  let use_only_paramod = bool "paramodulation" false in
+  let newauto = if use_only_paramod then true else newauto in
   let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
   let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
    if not newauto then