From ebfc19d792492417b129063fb511aa423e9d9e08 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 23 Feb 2015 22:27:53 +0100
Subject: Compensating 6fd763431 on postponing subtyping evar-evar problems.

Pushing pending problems had the side-effect of later solving them in
the opposite order as they arrived, resulting on different complexity
(see e.g. #4076). We now take care of pushing them in reverse order so
that they are treated in the same order.
---
 test-suite/complexity/bug4076.v | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)
 create mode 100644 test-suite/complexity/bug4076.v

(limited to 'test-suite/complexity')

diff --git a/test-suite/complexity/bug4076.v b/test-suite/complexity/bug4076.v
new file mode 100644
index 0000000000..2c87a908f4
--- /dev/null
+++ b/test-suite/complexity/bug4076.v
@@ -0,0 +1,29 @@
+(* Check behavior of evar-evar subtyping problems in the presence of
+   nested let-ins *)
+(* Expected time < 2.00s *)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Parameter f : forall P, forall (i : nat), P i -> P i.
+Parameter P : nat -> Type.
+
+Definition g (n : nat) (a0 : P n) : P n :=
+  let a1  := f a0 in
+  let a2  := f a1 in
+  let a3  := f a2 in
+  let a4  := f a3 in
+  let a5  := f a4 in
+  let a6  := f a5 in
+  let a7  := f a6 in
+  let a8  := f a7 in
+  let a9  := f a8 in
+  let a10 := f a9 in 
+  let a11 := f a10 in
+  let a12 := f a11 in
+  let a13 := f a12 in
+  let a14 := f a13 in
+  let a15 := f a14 in
+  let a16 := f a15 in
+  let a17 := f a16 in
+  a17.
-- 
cgit v1.2.3


From d1cbd0b21dd73e2b4af3ced394b51877afde40b8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 25 Feb 2015 14:00:33 +0100
Subject: Another test for a variant of complexity problem #4076 (thanks to A.
 Mortberg).

---
 test-suite/complexity/bug4076bis.v | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)
 create mode 100644 test-suite/complexity/bug4076bis.v

(limited to 'test-suite/complexity')

diff --git a/test-suite/complexity/bug4076bis.v b/test-suite/complexity/bug4076bis.v
new file mode 100644
index 0000000000..9303e60a21
--- /dev/null
+++ b/test-suite/complexity/bug4076bis.v
@@ -0,0 +1,31 @@
+(* Another check of evar-evar subtyping problems in the presence of
+   nested let-ins *)
+(* Expected time < 2.00s *)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+Parameter f : forall P, forall (i j : nat), P i j -> P i j.
+Parameter P : nat -> nat -> Type.
+
+Timeout 10 Definition g (n : nat) (a0 : P n n) : P n n :=
+  let a1  := f a0 in
+  let a2  := f a1 in
+  let a3  := f a2 in
+  let a4  := f a3 in
+  let a5  := f a4 in
+  let a6  := f a5 in
+  let a7  := f a6 in
+  let a8  := f a7 in
+  let a9  := f a8 in
+  let a10 := f a9 in 
+  let a11 := f a10 in
+  let a12 := f a11 in
+  let a13 := f a12 in
+  let a14 := f a13 in
+  let a15 := f a14 in
+  let a16 := f a15 in
+  let a17 := f a16 in
+  let a18 := f a17 in
+  let a19 := f a18 in
+  a19.
-- 
cgit v1.2.3


From 6fcfa31005273e3d5e0fac6fec9c0448e66a8780 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 26 Feb 2015 10:04:55 +0100
Subject: Fixing complexity tests for #4076.

---
 test-suite/complexity/bug4076.v    | 2 +-
 test-suite/complexity/bug4076bis.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'test-suite/complexity')

diff --git a/test-suite/complexity/bug4076.v b/test-suite/complexity/bug4076.v
index 2c87a908f4..3cf9e8b093 100644
--- a/test-suite/complexity/bug4076.v
+++ b/test-suite/complexity/bug4076.v
@@ -8,7 +8,7 @@ Unset Strict Implicit.
 Parameter f : forall P, forall (i : nat), P i -> P i.
 Parameter P : nat -> Type.
 
-Definition g (n : nat) (a0 : P n) : P n :=
+Time Definition g (n : nat) (a0 : P n) : P n :=
   let a1  := f a0 in
   let a2  := f a1 in
   let a3  := f a2 in
diff --git a/test-suite/complexity/bug4076bis.v b/test-suite/complexity/bug4076bis.v
index 9303e60a21..f3996e6ae6 100644
--- a/test-suite/complexity/bug4076bis.v
+++ b/test-suite/complexity/bug4076bis.v
@@ -8,7 +8,7 @@ Unset Strict Implicit.
 Parameter f : forall P, forall (i j : nat), P i j -> P i j.
 Parameter P : nat -> nat -> Type.
 
-Timeout 10 Definition g (n : nat) (a0 : P n n) : P n n :=
+Time Definition g (n : nat) (a0 : P n n) : P n n :=
   let a1  := f a0 in
   let a2  := f a1 in
   let a3  := f a2 in
-- 
cgit v1.2.3