]> matita.cs.unibo.it Git - helm.git/commitdiff
Sorry, bug introduced by me yesterday now fixed.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 10 Oct 2006 08:00:32 +0000 (08:00 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 10 Oct 2006 08:00:32 +0000 (08:00 +0000)
auto should be the new one even when the paramodulation flag is given.

helm/software/components/tactics/autoTactic.ml

index 25696d7945448532efe981a56979a6bb61398320..cdfcf8c73ec560dfaf887bb9540e0267e4503659 100644 (file)
@@ -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