From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 26 Oct 2006 11:31:22 +0000 (+0000)
Subject: More timeout added to autos here and there.
X-Git-Tag: 0.4.95@7852~843
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=30bc693172eccfcd1440aef51e3e7c5f4171ef67;p=helm.git

More timeout added to autos here and there.
---

diff --git a/matita/contribs/CoRN/algebra/Setoids.ma b/matita/contribs/CoRN/algebra/Setoids.ma
index 6b7bf781d..5fc3725cc 100644
--- a/matita/contribs/CoRN/algebra/Setoids.ma
+++ b/matita/contribs/CoRN/algebra/Setoids.ma
@@ -1248,7 +1248,7 @@ apply f. apply n1. apply m1.
 apply eq_symmetric_unfolded.assumption.
 apply eq_symmetric_unfolded.assumption.
 apply H.
-auto new.
+auto new timeout=100.
 qed.
 
 (*
diff --git a/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma b/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma
index be5f789a3..b86e5f296 100644
--- a/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma
+++ b/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma
@@ -23,10 +23,10 @@ theorem ceq_trans: \forall C. \xforall c1,c2. ceq C c1 c2 \to
 intros.
 
 (*
-apply ceq_intro; apply cle_trans; [|auto new|auto new||auto new|auto new].
+apply ceq_intro; apply cle_trans; [|auto new timeout=100|auto new timeout=100||auto new timeout=100|auto new timeout=100].
 qed.
 
 theorem ceq_sym: \forall C,c1,c2. ceq C c1 c2 \to ceq C c2 c1.
-intros; elim H; clear H.; auto new.
+intros; elim H; clear H.; auto new timeout=100.
 qed.
 *)
diff --git a/matita/contribs/RELATIONAL/NLE/dec.ma b/matita/contribs/RELATIONAL/NLE/dec.ma
index 3b4e0203a..7c45ab488 100644
--- a/matita/contribs/RELATIONAL/NLE/dec.ma
+++ b/matita/contribs/RELATIONAL/NLE/dec.ma
@@ -18,12 +18,12 @@ include "NLE/props.ma".
 
 theorem nat_dec_lt_ge: \forall x,y. x < y \lor y <= x.
  intros 2; elim y; clear y;
- [ auto new
+ [ auto new timeout=100
  | decompose;
    [ lapply linear nle_gen_succ_1 to H1. decompose.
-     subst. auto new depth=4
+     subst. auto new timeout=100 depth=4
    | lapply linear nle_lt_or_eq to H1; decompose;
-     subst; auto new
+     subst; auto new timeout=100
    ]
  ].
 qed.
diff --git a/matita/contribs/RELATIONAL/NLE/props.ma b/matita/contribs/RELATIONAL/NLE/props.ma
index 066e056e0..bd76c2754 100644
--- a/matita/contribs/RELATIONAL/NLE/props.ma
+++ b/matita/contribs/RELATIONAL/NLE/props.ma
@@ -17,20 +17,20 @@ set "baseuri" "cic:/matita/RELATIONAL/NLE/props".
 include "NLE/fwd.ma".
 
 theorem nle_refl: \forall x. x <= x.
- intros 1; elim x; clear x; intros; auto new.
+ intros 1; elim x; clear x; intros; auto new timeout=100.
 qed.
 
 theorem nle_trans_succ: \forall x,y. x <= y \to x <= succ y.
- intros. elim H; clear H x y; intros; auto new.
+ intros. elim H; clear H x y; intros; auto new timeout=100.
 qed.
 
 theorem nle_lt_or_eq: \forall y,x. x <= y \to x < y \lor x = y.
  intros 1. elim y; clear y; intros;
- [ lapply linear nle_gen_zero_2 to H. auto new
+ [ lapply linear nle_gen_zero_2 to H. auto new timeout=100
  | lapply linear nle_gen_succ_2 to H1. decompose;
-   [ subst. auto new
+   [ subst. auto new timeout=100
    | lapply linear H to H3 as H0. decompose;
-     subst; auto new
+     subst; auto new timeout=100
    ]
  ].
 qed.
diff --git a/matita/contribs/RELATIONAL/NPlus/props.ma b/matita/contribs/RELATIONAL/NPlus/props.ma
index 0c3379f62..2c908d1d0 100644
--- a/matita/contribs/RELATIONAL/NPlus/props.ma
+++ b/matita/contribs/RELATIONAL/NPlus/props.ma
@@ -17,7 +17,7 @@ set "baseuri" "cic:/matita/RELATIONAL/NPlus/props".
 include "NPlus/fwd.ma".
 
 theorem nplus_zero_1: \forall q. zero + q == q.
- intros. elim q; clear q; auto new.
+ intros. elim q; clear q; auto new timeout=100.
 qed.
 
 theorem nplus_succ_1: \forall p,q,r. NPlus p q r \to 
@@ -28,7 +28,7 @@ theorem nplus_succ_1: \forall p,q,r. NPlus p q r \to
  | lapply linear nplus_gen_succ_2 to H1 as H0.
    decompose.
    subst
- ]; auto new.
+ ]; auto new timeout=100.
 qed.
 
 theorem nplus_sym: \forall p,q,r. (p + q == r) \to q + p == r.
@@ -38,21 +38,21 @@ theorem nplus_sym: \forall p,q,r. (p + q == r) \to q + p == r.
  | lapply linear nplus_gen_succ_2 to H1 as H0.
    decompose.
    subst
- ]; auto new.
+ ]; auto new timeout=100.
 qed.
 
 theorem nplus_shift_succ_sx: \forall p,q,r. 
                              (p + (succ q) == r) \to (succ p) + q == r.
  intros.
  lapply linear nplus_gen_succ_2 to H as H0.
- decompose. subst. auto new.
+ decompose. subst. auto new timeout=100.
 qed.
 
 theorem nplus_shift_succ_dx: \forall p,q,r. 
                              ((succ p) + q == r) \to p + (succ q) == r.
  intros.
  lapply linear nplus_gen_succ_1 to H as H0.
- decompose. subst. auto new.
+ decompose. subst. auto new timeout=100.
 qed.
 
 theorem nplus_trans_1: \forall p,q1,r1. (p + q1 == r1) \to 
@@ -67,7 +67,7 @@ theorem nplus_trans_1: \forall p,q1,r1. (p + q1 == r1) \to
    decompose. subst.
    lapply linear H to H4, H3 as H0.
    decompose.
- ]; apply ex_intro; [| auto new || auto new ]. (**)
+ ]; apply ex_intro; [| auto new timeout=100 || auto new timeout=100 ]. (**)
 qed.
 
 theorem nplus_trans_2: \forall p1,q,r1. (p1 + q == r1) \to 
@@ -82,7 +82,7 @@ theorem nplus_trans_2: \forall p1,q,r1. (p1 + q == r1) \to
    decompose. subst.
    lapply linear H to H4, H3 as H0.
    decompose.
- ]; apply ex_intro; [| auto new || auto new ]. (**)
+ ]; apply ex_intro; [| auto new timeout=100 || auto new timeout=100 ]. (**)
 qed.
 
 theorem nplus_conf: \forall p,q,r1. (p + q == r1) \to 
@@ -94,5 +94,5 @@ theorem nplus_conf: \forall p,q,r1. (p + q == r1) \to
    decompose. subst.
    lapply linear nplus_gen_succ_2 to H2 as H0.
    decompose. subst.
- ]; auto new.
+ ]; auto new timeout=100.
 qed.