From 6fcfa31005273e3d5e0fac6fec9c0448e66a8780 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 26 Feb 2015 10:04:55 +0100
Subject: Fixing complexity tests for #4076.

---
 test-suite/complexity/bug4076.v    | 2 +-
 test-suite/complexity/bug4076bis.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/complexity/bug4076.v b/test-suite/complexity/bug4076.v
index 2c87a908f4..3cf9e8b093 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 9303e60a21..f3996e6ae6 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
-- 
cgit v1.2.3