From fc78a6baa572579f33fe82344077424aaf205c0e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 7 Apr 2016 19:09:20 +0200
Subject: [PATCH] Make atomic a boolean predicate.

---
 theories/decidable.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/theories/decidable.v b/theories/decidable.v
index 81c18b8f..ae6c6599 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -113,6 +113,7 @@ Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P → P.
 Proof. rewrite bool_decide_spec; trivial. Qed.
 Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P → bool_decide P.
 Proof. rewrite bool_decide_spec; trivial. Qed.
+Hint Resolve bool_decide_pack.
 Lemma bool_decide_true (P : Prop) `{Decision P} : P → bool_decide P = true.
 Proof. case_bool_decide; tauto. Qed.
 Lemma bool_decide_false (P : Prop) `{Decision P} : ¬P → bool_decide P = false.
-- 
GitLab