From d8965431f67e3786d5327f6e626e2f0f3c5d2f63 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 6 Nov 2016 12:21:01 +0100
Subject: [PATCH] Solve atomic obligations also by "assumption".

---
 program_logic/weakestpre.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index ffaa00fa5..59efd2377 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -314,3 +314,5 @@ Section proofmode_classes.
             (WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
   Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_atomic. Qed.
 End proofmode_classes.
+
+Hint Extern 0 (atomic _) => assumption : typeclass_instances.
-- 
GitLab