diff options
Diffstat (limited to 'test-suite/complexity/bug4076.v')
| -rw-r--r-- | test-suite/complexity/bug4076.v | 2 |
1 files changed, 1 insertions, 1 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 |