aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/complexity
diff options
context:
space:
mode:
authorGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-03-12 16:40:02 +0000
committerGravatar barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-03-12 16:40:02 +0000
commita28e2d94c7a0ee0c85d7f018115ffc2c64e62d5f (patch)
tree28edbc838b59e8f58f289eb11508499b6e4d23a2 /test-suite/complexity
parent74db2b0098893a5912d7480a259ad91664a86120 (diff)
fixed minor pbs with test cases
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12865 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/complexity')
-rw-r--r--test-suite/complexity/guard.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/complexity/guard.v b/test-suite/complexity/guard.v
index f64ffc259..387263e2f 100644
--- a/test-suite/complexity/guard.v
+++ b/test-suite/complexity/guard.v
@@ -1,6 +1,6 @@
(* Examples to check that the guard condition does not unfold
irrelevant subterms *)
-(* Expected time < 1s *)
+(* Expected time < 1.00s *)
Require Import Bool.
Fixpoint slow n :=