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 000000000..2c87a908f --- /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