aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/complexity
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-12-28 19:56:31 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-12-28 19:56:31 +0000
commitd17bd6a4838b0b181582c23e16c2225277ac1719 (patch)
tree7be146826f6da0f7f83f1ae3ccd25874e91778f9 /test-suite/complexity
parent380acdd0100d55cd908a96731365c1ce287e2d10 (diff)
Correction petits bugs du check de la test-suite
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9466 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/complexity')
-rw-r--r--test-suite/complexity/evars_subst.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/complexity/evars_subst.v b/test-suite/complexity/evars_subst.v
index d79d9f0e0..6f9f86a95 100644
--- a/test-suite/complexity/evars_subst.v
+++ b/test-suite/complexity/evars_subst.v
@@ -20,7 +20,7 @@
Variable P : Set -> Set.
Variable f : forall A : Set, A -> P A.
-Check
+Time Check
let _ := f _ 0 in
let _ := f _ 0 in
let _ := f _ 0 in