From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 14 Nov 2006 14:48:54 +0000 (+0000)
Subject: library=1 in obtain _ = _ by _.
X-Git-Tag: make_still_working~6672
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=inline;h=118c871b5f04a5f76f17e35f0520f2330abcfa72;p=helm.git

library=1 in obtain _ = _ by _.
---

diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml
index 75f56f2b6..7561281a8 100644
--- a/helm/software/components/tactics/declarative.ml
+++ b/helm/software/components/tactics/declarative.ml
@@ -150,7 +150,7 @@ let rewritingstep ~dbd lhs rhs just conclude =
    match just with
       None ->
        Tactics.auto ~dbd
-        ~params:["paramodulation","1"; "timeout","3"]
+        ~params:["paramodulation","1"; "timeout","3"; "library","1"]
     | Some just -> Tactics.apply just
   in
    match lhs with