X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fdeclarative.ml;h=7561281a854ddd5871a32a577e7912a064517abd;hb=df23acc7cd38047095f3920ce3a6054f545a039d;hp=75f56f2b683bdc9f53fe6c5769ec0b7a8dec81cb;hpb=2632e0520c373f191b81c3975385d77e71314ca7;p=helm.git

diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml
index 75f56f2b6..7561281a8 100644
--- a/components/tactics/declarative.ml
+++ b/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