From 118c871b5f04a5f76f17e35f0520f2330abcfa72 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 14 Nov 2006 14:48:54 +0000 Subject: [PATCH] library=1 in obtain _ = _ by _. --- helm/software/components/tactics/declarative.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- 2.39.2