diff options
Diffstat (limited to 'test-suite/complexity')
| -rw-r--r-- | test-suite/complexity/bug4076.v | 2 | ||||
| -rw-r--r-- | test-suite/complexity/bug4076bis.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/complexity/bug4076.v b/test-suite/complexity/bug4076.v index 2c87a908f..3cf9e8b09 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 9303e60a2..f3996e6ae 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 |