diff options
| author | Tej Chajed | 2019-08-25 14:43:51 -0400 |
|---|---|---|
| committer | Tej Chajed | 2019-08-25 14:43:51 -0400 |
| commit | 7b1ad001056087b46bf4ac9629cb86500026a22a (patch) | |
| tree | 0002b080b56a86e5e8bf3e89ad4527ecc64cf1ae | |
| parent | 09953295ea86eaf78c6688a1a2861aa6f41cd9ab (diff) | |
Make Bool.eqb_spec transparent
| -rw-r--r-- | theories/Bool/Bool.v | 2 |
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. |