The declarative rewriting step now tries auto timeout=3 before

[helm.git] / helm / software / components / tactics / declarative.ml

diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml
index 6c37acaa4fdfa1ae224ef2d5ae7945570a6e0cac..e36c860374cc8e109ec4d35068b1d87f3ea8ce5f 100644 (file)
--- a/helm/software/components/tactics/declarative.ml
+++ b/helm/software/components/tactics/declarative.ml
@@ -168,16 +168,22 @@ let rewritingstep ~dbd ~universe lhs rhs just last_step =
   let just =
    match just with
       `Auto params ->
-        let params =
-         if not (List.exists (fun (k,_) -> k = "paramodulation") params) then
-          ("paramodulation","1")::params
-         else params in
         let params =
          if not (List.exists (fun (k,_) -> k = "timeout") params) then
           ("timeout","3")::params
          else params
         in
-         Tactics.auto ~dbd ~params ~universe
+        let params' =
+         if not (List.exists (fun (k,_) -> k = "paramodulation") params) then
+          ("paramodulation","1")::params
+         else params
+        in
+         if params = params' then
+          Tactics.auto ~dbd ~params ~universe
+         else
+          Tacticals.first
+           [Tactics.auto ~dbd ~params ~universe ;
+            Tactics.auto ~dbd ~params:params' ~universe]
     | `Term just -> Tactics.apply just 
   in
    let plhs,prhs,prepare =