The default for paramodulation is now back to false (I set it to true

by mistake).

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 194f05dc936a62396bd5f253423faf5da865a13d..4acacefc6bd3f09eb583a385e75a2386f8f73908 100644 (file)
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -560,7 +560,7 @@ let flags_of_params params ?(for_applyS=false) () =
  let bool = bool params in
  let use_paramod = bool "use_paramod" true in
  let use_only_paramod =
-  if for_applyS then true else bool "paramodulation" true in
+  if for_applyS then true else bool "paramodulation" false in
  let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
  let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
  let timeout = int "timeout" 0 in