From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 12 Oct 2006 10:37:17 +0000 (+0000)
Subject: The default for paramodulation is now back to false (I set it to true
X-Git-Tag: make_still_working~6756
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7278063faf0ebb5fd08af2191989a12e2a27f522;p=helm.git

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 194f05dc9..4acacefc6 100644
--- 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