From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 20 Apr 2007 15:33:27 +0000 (+0000)
Subject: The declarative rewriting step now tries auto timeout=3 before
X-Git-Tag: make_still_working~6365
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=20fcf3075628a59f30db4cc3ce81ea0d0f410d3f;p=helm.git

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 6c37acaa4..e36c86037 100644
--- 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 6000a98ad..34bc2d4f3 100644
--- 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 :