diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-02-23 22:27:53 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-02-23 23:59:20 +0100 |
commit | ebfc19d792492417b129063fb511aa423e9d9e08 (patch) | |
tree | 229437122966d9bf18770982e68fa7a7895bf439 /test-suite/complexity | |
parent | d64b5766aa8de3842edae167ce554c36ff46f947 (diff) |
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.
Diffstat (limited to 'test-suite/complexity')
-rw-r--r-- | test-suite/complexity/bug4076.v | 29 |
1 files changed, 29 insertions, 0 deletions
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. |