From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 3 Oct 2006 15:58:50 +0000 (+0000)
Subject: Syntax of paramodulation parameters changed.
X-Git-Tag: 0.4.95@7852~935
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=23caa6768bc165f4145e0c8a19f6adb3dc2e4d6a;p=helm.git

Syntax of paramodulation parameters changed.
---

diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml
index 4dcf38b6d..c7e5579f8 100644
--- a/components/tactics/declarative.ml
+++ b/components/tactics/declarative.ml
@@ -130,7 +130,7 @@ let rewritingstep ~dbd lhs rhs just conclude =
    match just with
       None ->
        Tactics.auto ~dbd
-        ~params:["paramodulation","on"; "timeout","3"]
+        ~params:["paramodulation","1"; "timeout","3"]
     | Some just -> Tactics.apply just
   in
    match lhs with