9 files changed, 20 insertions, 8 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index ac65d3a52..9df3ba4ec 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1846,7 +1846,11 @@ and interp_tacarg ist gl = function
 (* Interprets an application node *)
 and interp_app loc ist gl fv largs =
   match fv with
-    | VFun(trace,olfun,var,body) ->
+      (* if var=[] this means that evaluation of body has been delayed
+         by val_interp, so it is not a tactic that expects arguments.
+         Otherwise Ltac goes into an infinite loop (val_interp puts
+         a VFun back on body, and then interp_app is called again...) *)
+    | VFun(trace,olfun,(_::_ as var),body) ->
       let (newlfun,lvar,lval)=head_with_value (var,largs) in
       if lvar=[] then
 	let v = 
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 _).
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 757cf6a4e..b1c645623 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -220,3 +220,11 @@ Z1 O.
 Z2 ltac:O.
 exact I.
 Qed.
+
+(* Illegal application used to make Ltac loop. *)
+
+Section LtacLoopTest.
+  Ltac f x := idtac.
+  Goal True.
+  Timeout 1 try f()().
+End LtacLoopTest.