aboutsummaryrefslogtreecommitdiff
path: root/test-suite/complexity/constructor.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/complexity/constructor.v')
-rw-r--r--test-suite/complexity/constructor.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/complexity/constructor.v b/test-suite/complexity/constructor.v
index c5e1953829..31217ca75e 100644
--- a/test-suite/complexity/constructor.v
+++ b/test-suite/complexity/constructor.v
@@ -214,3 +214,4 @@ Fixpoint expand (n : nat) : Prop :=
Example Expand : expand 2500.
Time constructor. (* ~0.45 secs *)
+Qed.