illegal tactic application was having Ltac interpreter loop

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11963 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 7 insertions, 7 deletions

diff --git a/test-suite/complexity/autodecomp.v b/test-suite/complexity/autodecomp.v
index 8916b1044..85589ff79 100644
--- a/test-suite/complexity/autodecomp.v
+++ b/test-suite/complexity/autodecomp.v
@@ -8,4 +8,4 @@ True/\True->
 True/\True->
 False/\False.
 
-Time auto decomp.
+Timeout 5 Time auto decomp.
diff --git a/test-suite/complexity/injection.v b/test-suite/complexity/injection.v
index eb01133e7..db2d9c53f 100644
--- a/test-suite/complexity/injection.v
+++ b/test-suite/complexity/injection.v
@@ -110,4 +110,4 @@ Lemma test: forall n1 w1 n2 w2, mk_world n1 w1 = mk_world n2 w2 ->
          n1 = n2.
 Proof.
 intros.
-Time injection H.
+Timeout 10 Time injection H.
diff --git a/test-suite/complexity/pretyping.v b/test-suite/complexity/pretyping.v
index c271fb50b..a884ea198 100644
--- a/test-suite/complexity/pretyping.v
+++ b/test-suite/complexity/pretyping.v
@@ -6,7 +6,7 @@ Require Import Ring_tac.
 
 Open Scope R_scope.
 
-Time Goal forall x1 x2 x3 y1 y2 y3 e1 e2 e3 e4 e5 e6 e7: R,
+Timeout 5 Time Goal forall x1 x2 x3 y1 y2 y3 e1 e2 e3 e4 e5 e6 e7: R,
 (e6 + e7 - 2 * y2 * y3 - x2 * e3 - x3 * e3 - e3 * x1) *
 ((e6 + e7 - 2 * y2 * y3 - x2 * e3 - x3 * e3 - e3 * x1) * 1) *
 ((- (y1 - y2) * (e5 + e6 - 2 * y1 * y2 - x1 * e1 - x2 * e1 - e1 * x1) -
diff --git a/test-suite/complexity/ring.v b/test-suite/complexity/ring.v
index 5a541bc24..51f7c4dab 100644
--- a/test-suite/complexity/ring.v
+++ b/test-suite/complexity/ring.v
@@ -4,4 +4,4 @@
 Require Import ZArith.
 Open Scope Z_scope.
 Goal forall a, a+a+a+a+a+a+a+a+a+a+a+a+a = a*13.
-Time intro; ring.
+Timeout 5 Time intro; ring.
diff --git a/test-suite/complexity/ring2.v b/test-suite/complexity/ring2.v
index e1a799f07..af678a2e1 100644
--- a/test-suite/complexity/ring2.v
+++ b/test-suite/complexity/ring2.v
@@ -48,4 +48,4 @@ Open Scope Z_scope.
 Infix "+" := Zplus : Z_scope.
 
 Goal forall a, a+a+a+a+a+a+a+a+a+a+a+a+a = a*13.
-Time intro; ring.
+Timeout 5 Time intro; ring.
diff --git a/test-suite/complexity/setoid_rewrite.v b/test-suite/complexity/setoid_rewrite.v
index 3b5a0de79..2e3b006ef 100644
--- a/test-suite/complexity/setoid_rewrite.v
+++ b/test-suite/complexity/setoid_rewrite.v
@@ -7,4 +7,4 @@ Variable f : nat -> Prop.
 
 Goal forall U:Prop, f 100 <-> U.
 intros U.
-Time setoid_replace U with False.
+Timeout 5 Time setoid_replace U with False.
diff --git a/test-suite/complexity/unification.v b/test-suite/complexity/unification.v
index 0e1ec00d6..d2ea52751 100644
--- a/test-suite/complexity/unification.v
+++ b/test-suite/complexity/unification.v
@@ -48,4 +48,4 @@ Goal
    ))))
    ))))
 .
-Time try refine (refl_equal _).
+Timeout 2 Time try refine (refl_equal _).