The declarative rewriting step now tries auto timeout=3 before

auto paramodulation timeout=3. This seems to work better then just
auto paramodulation alone when the user tries to help the system.
This because paramodulation is more confused than helped.

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 =

diff --git a/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli
index 6000a98ad3fed5cdbe7f168a100b647ca15451b8..34bc2d4f361907d667c62ccc818ae0b4fa3d5854 100644 (file)
--- a/helm/software/components/tactics/tactics.mli
+++ b/helm/software/components/tactics/tactics.mli
@@ -1,4 +1,4 @@
-(* GENERATED FILE, DO NOT EDIT. STAMP:Fri Apr 20 15:46:14 CEST 2007 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Fri Apr 20 17:07:53 CEST 2007 *)
 val absurd : term:Cic.term -> ProofEngineTypes.tactic
 val apply : term:Cic.term -> ProofEngineTypes.tactic
 val applyS :