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 000000000..9303e60a2 --- /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