Imported Upstream snapshot 8.3~beta0+13298

8 files changed, 40 insertions, 11 deletions

diff --git a/test-suite/complexity/autodecomp.v b/test-suite/complexity/autodecomp.v
index 8916b104..85589ff7 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 eb01133e..335996c2 100644
--- a/test-suite/complexity/injection.v
+++ b/test-suite/complexity/injection.v
@@ -43,11 +43,11 @@ Record joinmap (key: Type) (t: Type) (j : joinable t) : Type
             exists s2, jm_j.(join) s1 s2 s3
 }.
 
-Parameter mkJoinmap :   forall (key: Type) (t: Type) (j: joinable t), 
+Parameter mkJoinmap :   forall (key: Type) (t: Type) (j: joinable t),
 joinmap key j.
 
 Parameter ADMIT: forall p: Prop, p.
-Implicit Arguments ADMIT [p].    
+Implicit Arguments ADMIT [p].
 
 Module Share.
 Parameter jb : joinable bool.
@@ -90,7 +90,7 @@ Definition jown : joinable own :=
   Joinable own_is_empty own_join
      ADMIT ADMIT  ADMIT  ADMIT  ADMIT  ADMIT  ADMIT  ADMIT .
 End Own.
-  
+
 Fixpoint sinv (n: nat) : Type :=
   match n with
    | O => unit
@@ -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/lettuple.v b/test-suite/complexity/lettuple.v
new file mode 100644
index 00000000..0690459f
--- /dev/null
+++ b/test-suite/complexity/lettuple.v
@@ -0,0 +1,29 @@
+(* This example checks if printing nested let-in's stays in linear time *)
+(* Expected time < 1.00s *)
+
+Definition f (x : nat * nat) :=
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  let (a,b) := x in
+  0.
+
+Timeout 5 Time Print f.
diff --git a/test-suite/complexity/pretyping.v b/test-suite/complexity/pretyping.v
index c271fb50..a884ea19 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 5a541bc2..51f7c4da 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 e1a799f0..ab57afdb 100644
--- a/test-suite/complexity/ring2.v
+++ b/test-suite/complexity/ring2.v
@@ -1,4 +1,4 @@
-(* This example, checks the efficiency of the abstract machine used by ring *)
+(* This example checks the efficiency of the abstract machine used by ring *)
 (* Expected time < 1.00s *)
 
 Require Import BinInt Zbool.
@@ -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 3b5a0de7..2e3b006e 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 0e1ec00d..d2ea5275 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 _).