diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-02-26 10:04:55 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-02-26 10:04:55 +0100 |
| commit | 6fcfa31005273e3d5e0fac6fec9c0448e66a8780 (patch) | |
| tree | 41b68cbcf3646256c92c8bfe8238fb7b5c23f901 /test-suite/complexity | |
| parent | 9dacc590c604290d9556d9368c5c735321e01e90 (diff) | |
Fixing complexity tests for #4076.
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 |