diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 13:15:50 +0200 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 13:15:50 +0200 |
commit | e347929583f820a2cc0296597b6382309e930989 (patch) | |
tree | cdc3f18fc5c66a9d3d7cc8404c6a295169e41fcc /test-suite/complexity/bug4076.v | |
parent | c01be74d81a5466c58f8dc6c568db286b0979997 (diff) | |
parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) |
Merge tag 'upstream/8.5_beta2+dfsg' into test
Upstream version 8.5~beta2+dfsg
Diffstat (limited to 'test-suite/complexity/bug4076.v')
-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 00000000..3cf9e8b0 --- /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. + +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 + 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. |