Sorry, bug introduced by me yesterday now fixed.

auto should be the new one even when the paramodulation flag is given.

diff --git a/helm/software/components/tactics/autoTactic.ml b/helm/software/components/tactics/autoTactic.ml
index 25696d7945448532efe981a56979a6bb61398320..cdfcf8c73ec560dfaf887bb9540e0267e4503659 100644 (file)
--- 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