]> matita.cs.unibo.it Git - helm.git/commitdiff
library=1 in obtain _ = _ by _.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 14 Nov 2006 14:48:54 +0000 (14:48 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 14 Nov 2006 14:48:54 +0000 (14:48 +0000)
components/tactics/declarative.ml

index 75f56f2b683bdc9f53fe6c5769ec0b7a8dec81cb..7561281a854ddd5871a32a577e7912a064517abd 100644 (file)
@@ -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