aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/complexity
diff options
context:
space:
mode:
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