aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--theories/Bool/Bool.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 0c0a1897a8..296c253363 100644
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -822,4 +822,4 @@ Defined.
Lemma eqb_spec (b b' : bool) : reflect (b = b') (eqb b b').
Proof.
destruct b, b'; now constructor.
-Qed.
+Defined.