diff --git a/Makefile b/Makefile
index f023f15a1eea76c6eadd3719bda1d68ad5cba621..2623cc780af21d1d2251be80e813486ae5681604 100644
--- a/Makefile
+++ b/Makefile
@@ -28,16 +28,15 @@ build-dep: build-dep/opam phony
 	@# constraints.  Otherwise, `opam upgrade` may well update some packages to versions
 	@# that are incompatible with our build requirements.
 	@# To achieve this, we create a fake opam package that has our build-dependencies as
-	@# dependencies, but does not actually install anything.
-	@# Reinstalling is needed with opam 1 in case the pin already exists, but the builddep
-	@# package changed.
-	@BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
-	  echo "# Pinning build-dep package." && \
-	  opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
-	  ((! opam --version | grep "^1\." > /dev/null) || ( \
-	    echo "# Reinstalling build-dep package." && \
-	    opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE" \
-	  ))
+	@# dependencies, but does not actually install anything itself.
+	@echo "# Pinning build-dep package." && \
+	  if opam --version | grep "^1\." -q; then \
+	    BUILD_DEP_PACKAGE="$$(egrep "^name:" build-dep/opam | sed 's/^name: *"\(.*\)" */\1/')" && \
+	    opam pin add -k path $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE".dev build-dep && \
+	    opam reinstall $(OPAMFLAGS) "$$BUILD_DEP_PACKAGE"; \
+	  else \
+	    opam install $(OPAMFLAGS) build-dep/; \
+	  fi
 
 # Some files that do *not* need to be forwarded to Makefile.coq
 Makefile: ;
diff --git a/Makefile.coq.local b/Makefile.coq.local
index 0c66b18a155dcf3d0b7d34a5d778c991ca97dab1..320d96b05c3177332858a0ec1919c472043a1dcf 100644
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -11,11 +11,6 @@ COQ_TEST=$(COQTOP) $(COQDEBUG) -batch -test-mode
 COQ_OLD=$(shell echo "$(COQ_VERSION)" | egrep "^8\.7\b" -q && echo 1)
 COQ_MINOR_VERSION=$(shell echo "$(COQ_VERSION)" | egrep '^[0-9]+\.[0-9]+\b' -o)
 
-# Can't use pipes because that discards error codes and dash provides no way to control that.
-# Also egrep errors if it doesn't match anything, we have to ignore that.
-# Oh Unix...
-REF_FILTER=egrep -v '(^Welcome to Coq|^Skipping rcfile loading.$$)'
-
 tests/.coqdeps.d: $(TESTFILES)
 	$(SHOW)'COQDEP TESTFILES'
 	$(HIDE)$(COQDEP) -dyndep var $(COQMF_COQLIBS_NOML) $^ $(redir_if_ok)
@@ -28,13 +23,12 @@ $(TESTFILES:.v=.vo): %.vo: %.v $(if $(MAKE_REF),,%.ref)
 	  else \
 	    REF="tests/$$TEST.ref"; \
 	  fi && \
-	  echo $(if $(MAKE_REF),"COQTEST [ref] `basename "$$REF"`","COQTEST$(if $(COQ_OLD), [ignored],) `basename "$$REF"`") && \
+	  echo $(if $(MAKE_REF),"COQTEST [make ref] `basename "$$REF"`","COQTEST$(if $(COQ_OLD), [ignored],) `basename "$$REF"`") && \
 	  TMPFILE="$$(mktemp)" && \
 	  $(TIMER) $(COQ_TEST) $(COQFLAGS) $(COQLIBS) -load-vernac-source $< > "$$TMPFILE" && \
-	  ($(REF_FILTER) < "$$TMPFILE" > "$$TMPFILE.filtered" || true) && \
 	  $(if $(MAKE_REF), \
-	    mv "$$TMPFILE.filtered" "$$REF", \
-	    $(if $(COQ_OLD),true,diff -u "$$REF" "$$TMPFILE.filtered") \
+	    mv "$$TMPFILE" "$$REF", \
+	    $(if $(COQ_OLD),true,diff -u "$$REF" "$$TMPFILE") \
 	  ) && \
-	  rm -f "$$TMPFILE" "$$TMPFILE.filtered" && \
+	  rm -f "$$TMPFILE" && \
 	  touch $@
diff --git a/README.md b/README.md
index 07a61c6ece051a0388ee56f003eefe59f7eba75e..35a8e29a7ce035d9d87210fa872241f06ba06579 100644
--- a/README.md
+++ b/README.md
@@ -105,8 +105,6 @@ that should be compatible with this version:
   formalization of the core Rust type system.
 * [iGPS](https://gitlab.mpi-sws.org/FP/sra-gps/tree/gen_proofmode_WIP) is a
   logic for release-acquire memory.
-* [Iris Atomic](https://gitlab.mpi-sws.org/iris/atomic) is an experimental
-  formalization of logically atomic triples in Iris.
 * [Iron](https://gitlab.mpi-sws.org/iris/iron) is a linear separation logic
   built on top of Iris for precise reasoning about resources (such as making
   sure there are no memory leaks).
diff --git a/opam b/opam
index 0b17ee15f1cb7d97e73351db0d3e1b1018685061..8d79131fab59386878b59d5c206eb226baadd18a 100644
--- a/opam
+++ b/opam
@@ -11,5 +11,5 @@ install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
 depends: [
   "coq" { (>= "8.7.1" & < "8.10~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2019-01-24.2.b72e1fa8") | (= "dev") }
+  "coq-stdpp" { (= "dev.2019-01-25.1.26088f98") | (= "dev") }
 ]
diff --git a/tests/atomic.8.8.ref b/tests/atomic.8.8.ref
index 238708315a1656731ecc3a853489338db7c99e9d..a3f9185273b897d0d0eebbbde3e4ec0a5bd52004 100644
--- a/tests/atomic.8.8.ref
+++ b/tests/atomic.8.8.ref
@@ -1,3 +1,17 @@
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  aheap : atomic_heap Σ
+  Q : iProp Σ
+  l : loc
+  v : val
+  ============================
+  "Hl" : l ↦ v
+  --------------------------------------∗
+  AACC << ∀ (v0 : val) (q : Qp), l ↦{q} v0 ABORT l ↦ v >> @ ⊤, ∅
+       << l ↦{q} v0, COMM Q -∗ Q >>
+  
 1 subgoal
   
   Σ : gFunctors
@@ -10,11 +24,9 @@
   Σ : gFunctors
   heapG0 : heapG Σ
   P : val → iProp Σ
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
-  "AU" : AU << ∀ x : val, P x >> @ ⊤, ∅ << ∃ y : val, P y, COMM Q -∗ Φ #() >>
+  "AU" : AU << ∀ x : val, P x >> @ ⊤, ∅ << ∃ y : val, P y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -23,14 +35,12 @@
   Σ : gFunctors
   heapG0 : heapG Σ
   P : val → iProp Σ
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
   _ : AACC << ∀ x : val, P x
               ABORT AU << ∀ x : val, P x >> @ ⊤, ∅
-                       << ∃ y : val, P y, COMM Q -∗ Φ #() >> >> @ ⊤, ∅
-           << ∃ y : val, P y, COMM Q -∗ Φ #() >>
+                       << ∃ y : val, P y, COMM Φ #() >> >> @ ⊤, ∅
+           << ∃ y : val, P y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -46,11 +56,9 @@
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
-  "AU" : AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Q -∗ Φ #() >>
+  "AU" : AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -59,14 +67,11 @@
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
   _ : AACC << ∀ x : val, l ↦ x
-              ABORT AU << ∀ x : val, l ↦ x >> @ ⊤, ∅
-                       << l ↦ x, COMM Q -∗ Φ #() >> >> @ ⊤, ∅
-           << l ↦ x, COMM Q -∗ Φ #() >>
+              ABORT AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Φ #() >> >> 
+           @ ⊤, ∅ << l ↦ x, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -82,11 +87,9 @@
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
-  "AU" : AU << l ↦ #() >> @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
+  "AU" : AU << l ↦ #() >> @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -95,14 +98,12 @@
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
   _ : AACC << l ↦ #()
               ABORT AU << l ↦ #() >> @ ⊤, ∅
-                       << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >> >> @ ⊤, ∅
-           << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
+                       << ∃ y : val, l ↦ y, COMM Φ #() >> >> @ ⊤, ∅
+           << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -118,11 +119,9 @@
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
-  "AU" : AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >>
+  "AU" : AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -131,13 +130,11 @@
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
   _ : AACC << l ↦ #()
-              ABORT AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >> >> 
-           @ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >>
+              ABORT AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Φ #() >> >> 
+           @ ⊤, ∅ << l ↦ #(), COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -155,12 +152,10 @@
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
   "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x >> @ ⊤, ∅
-            << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
+            << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -178,12 +173,10 @@
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
   "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
-            @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
+            @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -202,14 +195,12 @@
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
   _ : AU << ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
          << ∃ yyyy : val, l ↦ yyyy
                           ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
-            COMM Q -∗ Φ #() >>
+            COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -227,12 +218,10 @@
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
   "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
-            << l ↦ x, COMM Q -∗ Φ #() >>
+            << l ↦ x, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -252,12 +241,10 @@
   heapG0 : heapG Σ
   l : loc
   x : val
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
   "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
-            << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
+            << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -277,12 +264,10 @@
   heapG0 : heapG Σ
   l : loc
   x : val
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
   "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
-            << l ↦ #(), COMM Q -∗ Φ #() >>
+            << l ↦ #(), COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -302,12 +287,10 @@
   heapG0 : heapG Σ
   l : loc
   xx, yyyy : val
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
   "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
-            @ ⊤, ∅ << l ↦ yyyy, COMM Q -∗ Φ #() >>
+            @ ⊤, ∅ << l ↦ yyyy, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -328,31 +311,16 @@
   heapG0 : heapG Σ
   l : loc
   xx, yyyy : val
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
   "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
             << l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
-               COMM Q -∗ Φ #() >>
+               COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
 "Prettification"
      : string
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  P : val → iProp Σ
-  ============================
-  --------------------------------------∗
-  ∀ Φ : language.val heap_lang → iProp Σ, AU << ∀ 
-                                             x : val, 
-                                             P x >> @ ⊤, ∅
-                                             << ∃ y : val, P y, COMM Φ #() >>
-                                          -∗ WP ! #0 {{ v, Φ v }}
-  
 1 subgoal
   
   Σ : gFunctors
diff --git a/tests/atomic.ref b/tests/atomic.ref
index c51ade4ecb45eae71cc5255da2e926e868412fbc..6184f371c9cb452e5276630face9bbee9598cc9a 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -1,3 +1,17 @@
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  aheap : atomic_heap Σ
+  Q : iProp Σ
+  l : loc
+  v : val
+  ============================
+  "Hl" : l ↦ v
+  --------------------------------------∗
+  AACC << ∀ (v0 : val) (q : Qp), l ↦{q} v0 ABORT l ↦ v >> @ ⊤, ∅
+       << l ↦{q} v0, COMM Q -∗ Q >>
+  
 1 subgoal
   
   Σ : gFunctors
@@ -10,11 +24,9 @@
   Σ : gFunctors
   heapG0 : heapG Σ
   P : val → iProp Σ
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
-  "AU" : AU << ∀ x : val, P x >> @ ⊤, ∅ << ∃ y : val, P y, COMM Q -∗ Φ #() >>
+  "AU" : AU << ∀ x : val, P x >> @ ⊤, ∅ << ∃ y : val, P y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -23,14 +35,12 @@
   Σ : gFunctors
   heapG0 : heapG Σ
   P : val → iProp Σ
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
   _ : AACC << ∀ x : val, P x
               ABORT AU << ∀ x : val, P x >> @ ⊤, ∅
-                       << ∃ y : val, P y, COMM Q -∗ Φ #() >> >> @ ⊤, ∅
-           << ∃ y : val, P y, COMM Q -∗ Φ #() >>
+                       << ∃ y : val, P y, COMM Φ #() >> >> @ ⊤, ∅
+           << ∃ y : val, P y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -46,11 +56,9 @@
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
-  "AU" : AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Q -∗ Φ #() >>
+  "AU" : AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -59,14 +67,11 @@
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
   _ : AACC << ∀ x : val, l ↦ x
-              ABORT AU << ∀ x : val, l ↦ x >> @ ⊤, ∅
-                       << l ↦ x, COMM Q -∗ Φ #() >> >> @ ⊤, ∅
-           << l ↦ x, COMM Q -∗ Φ #() >>
+              ABORT AU << ∀ x : val, l ↦ x >> @ ⊤, ∅ << l ↦ x, COMM Φ #() >> >> 
+           @ ⊤, ∅ << l ↦ x, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -82,11 +87,9 @@
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
-  "AU" : AU << l ↦ #() >> @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
+  "AU" : AU << l ↦ #() >> @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -95,14 +98,12 @@
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
   _ : AACC << l ↦ #()
               ABORT AU << l ↦ #() >> @ ⊤, ∅
-                       << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >> >> @ ⊤, ∅
-           << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
+                       << ∃ y : val, l ↦ y, COMM Φ #() >> >> @ ⊤, ∅
+           << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -118,11 +119,9 @@
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
-  "AU" : AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >>
+  "AU" : AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -131,13 +130,11 @@
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
   _ : AACC << l ↦ #()
-              ABORT AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >> >> 
-           @ ⊤, ∅ << l ↦ #(), COMM Q -∗ Φ #() >>
+              ABORT AU << l ↦ #() >> @ ⊤, ∅ << l ↦ #(), COMM Φ #() >> >> 
+           @ ⊤, ∅ << l ↦ #(), COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -155,12 +152,10 @@
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
   "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x >> @ ⊤, ∅
-            << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
+            << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -178,12 +173,10 @@
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
   "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>
-            @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
+            @ ⊤, ∅ << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -202,14 +195,12 @@
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
   _ : AU << ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
          << ∃ yyyy : val, l ↦ yyyy
                           ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
-            COMM Q -∗ Φ #() >>
+            COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -227,12 +218,10 @@
   Σ : gFunctors
   heapG0 : heapG Σ
   l : loc
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
   "AU" : AU << ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
-            << l ↦ x, COMM Q -∗ Φ #() >>
+            << l ↦ x, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -252,12 +241,10 @@
   heapG0 : heapG Σ
   l : loc
   x : val
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
   "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
-            << ∃ y : val, l ↦ y, COMM Q -∗ Φ #() >>
+            << ∃ y : val, l ↦ y, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -277,12 +264,10 @@
   heapG0 : heapG Σ
   l : loc
   x : val
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
   "AU" : AU << l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >> @ ⊤, ∅
-            << l ↦ #(), COMM Q -∗ Φ #() >>
+            << l ↦ #(), COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -302,12 +287,10 @@
   heapG0 : heapG Σ
   l : loc
   xx, yyyy : val
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
   "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>
-            @ ⊤, ∅ << l ↦ yyyy, COMM Q -∗ Φ #() >>
+            @ ⊤, ∅ << l ↦ yyyy, COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
@@ -328,29 +311,16 @@
   heapG0 : heapG Σ
   l : loc
   xx, yyyy : val
-  Q : iPropI Σ
   Φ : language.val heap_lang → iProp Σ
   ============================
-  _ : Q
   "AU" : AU << l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >> @ ⊤, ∅
             << l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
-               COMM Q -∗ Φ #() >>
+               COMM Φ #() >>
   --------------------------------------∗
   WP code {{ v, Φ v }}
   
 "Prettification"
      : string
-1 subgoal
-  
-  Σ : gFunctors
-  heapG0 : heapG Σ
-  P : val → iProp Σ
-  ============================
-  --------------------------------------∗
-  ∀ Φ : language.val heap_lang → iProp Σ,
-    AU << ∀ x : val, P x >> @ ⊤, ∅ << ∃ y : val, P y, COMM Φ #() >>
-    -∗ WP ! #0 {{ v, Φ v }}
-  
 1 subgoal
   
   Σ : gFunctors
diff --git a/tests/atomic.v b/tests/atomic.v
index 9f2b7dd34229a244f597cbfa719ea7afbe02445a..236ec1e71c6f641b70281fc407182ab11ac2d497 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -1,9 +1,22 @@
 From iris.heap_lang Require Export lifting notation.
 From iris.program_logic Require Export atomic.
 From iris.proofmode Require Import tactics.
-From iris.heap_lang Require Import proofmode notation.
+From iris.heap_lang Require Import proofmode notation atomic_heap.
 Set Default Proof Using "Type".
 
+Section tests.
+  Context `{!heapG Σ} {aheap: atomic_heap Σ}.
+  Import atomic_heap.notation.
+
+  (* FIXME: removing the `val` type annotation breaks printing. *)
+  Lemma test_awp_apply_without (Q : iProp Σ) (l : loc) v :
+    Q -∗ l ↦ v -∗ WP !#l {{ _, Q }}.
+  Proof.
+    iIntros "HQ Hl". awp_apply load_spec without "HQ". Show.
+    iAaccIntro with "Hl"; eauto with iFrame.
+  Qed.
+End tests.
+
 (* Test if AWP and the AU obtained from AWP print. *)
 Section printing.
   Context `{!heapG Σ}.
@@ -13,28 +26,28 @@ Section printing.
   Lemma print_both_quant (P : val → iProp Σ) :
     <<< ∀ x, P x >>> code @ ⊤ <<< ∃ y, P y, RET #() >>>.
   Proof.
-    Show. iIntros (Q Φ) "? AU". Show.
+    Show. iIntros (Φ) "AU". Show.
     iPoseProof (aupd_aacc with "AU") as "?". Show.
   Abort.
 
   Lemma print_first_quant l :
     <<< ∀ x, l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>.
   Proof.
-    Show. iIntros (Q Φ) "? AU". Show.
+    Show. iIntros (Φ) "AU". Show.
     iPoseProof (aupd_aacc with "AU") as "?". Show.
   Abort.
 
   Lemma print_second_quant l :
     <<< l ↦ #() >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
   Proof.
-    Show. iIntros (Q Φ) "? AU". Show.
+    Show. iIntros (Φ) "AU". Show.
     iPoseProof (aupd_aacc with "AU") as "?". Show.
   Abort.
 
   Lemma print_no_quant l :
     <<< l ↦ #() >>> code @ ⊤ <<< l ↦ #(), RET #() >>>.
   Proof.
-    Show. iIntros (Q Φ) "? AU". Show.
+    Show. iIntros (Φ) "AU". Show.
     iPoseProof (aupd_aacc with "AU") as "?". Show.
   Abort.
 
@@ -43,49 +56,49 @@ Section printing.
   Lemma print_both_quant_long l :
     <<< ∀ x, l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
   Proof.
-    Show. iIntros (Q Φ) "? AU". Show.
+    Show. iIntros (Φ) "AU". Show.
   Abort.
 
   Lemma print_both_quant_longpre l :
     <<< ∀ x, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
   Proof.
-    Show. iIntros (Q Φ) "? AU". Show.
+    Show. iIntros (Φ) "AU". Show.
   Abort.
 
   Lemma print_both_quant_longpost l :
     <<< ∀ xx, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ⊤ <<< ∃ yyyy, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx, RET #() >>>.
   Proof.
-    Show. iIntros (Q Φ) "? ?". Show.
+    Show. iIntros (Φ) "?". Show.
   Abort.
 
   Lemma print_first_quant_long l :
     <<< ∀ x, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>.
   Proof.
-    Show. iIntros (Q Φ) "? AU". Show.
+    Show. iIntros (Φ) "AU". Show.
   Abort.
 
   Lemma print_second_quant_long l x :
     <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y, l ↦ y, RET #() >>>.
   Proof.
-    Show. iIntros (Q Φ) "? AU". Show.
+    Show. iIntros (Φ) "AU". Show.
   Abort.
 
   Lemma print_no_quant_long l x :
     <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< l ↦ #(), RET #() >>>.
   Proof.
-    Show. iIntros (Q Φ) "? AU". Show.
+    Show. iIntros (Φ) "AU". Show.
   Abort.
 
   Lemma print_no_quant_longpre l xx yyyy :
     <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ⊤ <<< l ↦ yyyy, RET #() >>>.
   Proof.
-    Show. iIntros (Q Φ) "? AU". Show.
+    Show. iIntros (Φ) "AU". Show.
   Abort.
 
   Lemma print_no_quant_longpost l xx yyyy :
     <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>> code @ ⊤ <<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx, RET #() >>>.
   Proof.
-    Show. iIntros (Q Φ) "? AU". Show.
+    Show. iIntros (Φ) "AU". Show.
   Abort.
 
   Check "Prettification".
@@ -93,7 +106,6 @@ Section printing.
   Lemma iMod_prettify (P : val → iProp Σ) :
     <<< ∀ x, P x >>> !#0 @ ⊤ <<< ∃ y, P y, RET #() >>>.
   Proof.
-    iApply wp_atomic_intro. Show.
     iIntros (Φ) "AU". iMod "AU". Show.
   Abort.
 
diff --git a/theories/heap_lang/lib/atomic_heap.v b/theories/heap_lang/lib/atomic_heap.v
index c88ba0204173197176eec74c2ba60805ad40733c..e5d4804bc6b1a592e9c3f40c5f4084e8725b67b0 100644
--- a/theories/heap_lang/lib/atomic_heap.v
+++ b/theories/heap_lang/lib/atomic_heap.v
@@ -81,18 +81,18 @@ Section proof.
     <<< ∀ (v : val) q, l ↦{q} v >>> primitive_load #l @ ⊤
     <<< l ↦{q} v, RET v >>>.
   Proof.
-    iIntros (Q Φ) "? AU". wp_lam.
+    iIntros (Φ) "AU". wp_lam.
     iMod "AU" as (v q) "[H↦ [_ Hclose]]".
-    wp_load. iMod ("Hclose" with "H↦") as "HΦ". by iApply "HΦ".
+    wp_load. iMod ("Hclose" with "H↦") as "HΦ". done.
   Qed.
 
   Lemma primitive_store_spec (l : loc) (w : val) :
     <<< ∀ v, l ↦ v >>> primitive_store #l w @ ⊤
     <<< l ↦ w, RET #() >>>.
   Proof.
-    iIntros (Q Φ) "? AU". wp_lam. wp_let.
+    iIntros (Φ) "AU". wp_lam. wp_let.
     iMod "AU" as (v) "[H↦ [_ Hclose]]".
-    wp_store. iMod ("Hclose" with "H↦") as "HΦ". by iApply "HΦ".
+    wp_store. iMod ("Hclose" with "H↦") as "HΦ". done.
   Qed.
 
   Lemma primitive_cas_spec (l : loc) (w1 w2 : val) :
@@ -102,10 +102,10 @@ Section proof.
     <<< if decide (v = w1) then l ↦ w2 else l ↦ v,
         RET #(if decide (v = w1) then true else false) >>>.
   Proof.
-    iIntros (? Q Φ) "? AU". wp_lam. wp_let. wp_let.
+    iIntros (? Φ) "AU". wp_lam. wp_let. wp_let.
     iMod "AU" as (v) "[H↦ [_ Hclose]]".
     destruct (decide (v = w1)) as [<-|Hv]; [wp_cas_suc|wp_cas_fail];
-    iMod ("Hclose" with "H↦") as "HΦ"; by iApply "HΦ".
+    iMod ("Hclose" with "H↦") as "HΦ"; done.
   Qed.
 End proof.
 
diff --git a/theories/heap_lang/lib/coin_flip.v b/theories/heap_lang/lib/coin_flip.v
index 885298940c3d118dae418194f590971aa91f7303..57b085436cbc529a968614e52528d67b8272b304 100644
--- a/theories/heap_lang/lib/coin_flip.v
+++ b/theories/heap_lang/lib/coin_flip.v
@@ -50,7 +50,7 @@ Section coinflip.
         @ ⊤
     <<< ∃ (b: bool), x ↦ #0, RET #b >>>.
   Proof.
-    iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam.
+    iIntros (Φ) "AU". wp_lam.
     wp_apply rand_spec; first done.
     iIntros (b) "_". wp_let.
     wp_bind (_ <- _)%E.
@@ -73,7 +73,7 @@ Section coinflip.
         @ ⊤
     <<< ∃ (b: bool), x ↦ #0, RET #b >>>.
   Proof.
-    iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam.
+    iIntros (Φ) "AU". wp_lam.
     wp_apply wp_new_proph; first done.
     iIntros (v p) "Hp".
     wp_let.
diff --git a/theories/heap_lang/lib/increment.v b/theories/heap_lang/lib/increment.v
index 6fd0a421562ef871c647f24e336f670a11175a3a..79f600e20796460be3f67970f9e6e9f11fd0b463 100644
--- a/theories/heap_lang/lib/increment.v
+++ b/theories/heap_lang/lib/increment.v
@@ -23,7 +23,7 @@ Section increment_physical.
   Lemma incr_phy_spec (l: loc) :
     <<< ∀ (v : Z), l ↦ #v >>> incr_phy #l @ ⊤ <<< l ↦ #(v + 1), RET #v >>>.
   Proof.
-    iApply wp_atomic_intro. iIntros (Φ) "AU". iLöb as "IH". wp_lam.
+    iIntros (Φ) "AU". iLöb as "IH". wp_lam.
     wp_bind (!_)%E. iMod "AU" as (v) "[Hl [Hclose _]]".
     wp_load. iMod ("Hclose" with "Hl") as "AU". iModIntro.
     wp_pures. wp_bind (CAS _ _ _)%E. iMod "AU" as (w) "[Hl Hclose]".
@@ -55,24 +55,24 @@ Section increment.
   Lemma incr_spec_direct (l: loc) :
     <<< ∀ (v : Z), l ↦ #v >>> incr #l @ ⊤ <<< l ↦ #(v + 1), RET #v >>>.
   Proof.
-    iApply wp_atomic_intro. iIntros (Φ) "AU". iLöb as "IH". wp_lam.
-    wp_apply load_spec; first by iAccu.
+    iIntros (Φ) "AU". iLöb as "IH". wp_lam.
+    awp_apply load_spec.
     (* Prove the atomic update for load *)
-    iAuIntro. rewrite /atomic_acc /=. iMod "AU" as (v) "[Hl [Hclose _]]".
+    rewrite /atomic_acc /=. iMod "AU" as (v) "[Hl [Hclose _]]".
     iModIntro. iExists _, _. iFrame "Hl". iSplit.
     { (* abort case *) done. }
-    iIntros "Hl". iMod ("Hclose" with "Hl") as "AU". iIntros "!> _".
+    iIntros "Hl". iMod ("Hclose" with "Hl") as "AU". iModIntro.
     (* Now go on *)
-    wp_apply cas_spec; [done|iAccu|].
+    awp_apply cas_spec; first done.
     (* Prove the atomic update for CAS *)
-    iAuIntro. rewrite /atomic_acc /=. iMod "AU" as (w) "[Hl Hclose]".
+    rewrite /atomic_acc /=. iMod "AU" as (w) "[Hl Hclose]".
     iModIntro. iExists _. iFrame "Hl". iSplit.
     { (* abort case *) iDestruct "Hclose" as "[? _]". done. }
     iIntros "Hl". destruct (decide (#w = #v)) as [[= ->]|Hx].
     - iDestruct "Hclose" as "[_ Hclose]". iMod ("Hclose" with "Hl") as "HΦ".
-      iIntros "!> _". wp_if. by iApply "HΦ".
+      iIntros "!>". wp_if. by iApply "HΦ".
     - iDestruct "Hclose" as "[Hclose _]". iMod ("Hclose" with "Hl") as "AU".
-      iIntros "!> _". wp_if. iApply "IH". done.
+      iIntros "!>". wp_if. iApply "IH". done.
   Qed.
 
   (** A proof of the incr specification that uses lemmas to avoid reasining
@@ -80,22 +80,22 @@ Section increment.
   Lemma incr_spec (l: loc) :
     <<< ∀ (v : Z), l ↦ #v >>> incr #l @ ⊤ <<< l ↦ #(v + 1), RET #v >>>.
   Proof.
-    iApply wp_atomic_intro. iIntros (Φ) "AU". iLöb as "IH". wp_lam.
-    wp_apply load_spec; first by iAccu.
+    iIntros (Φ) "AU". iLöb as "IH". wp_lam.
+    awp_apply load_spec.
     (* Prove the atomic update for load *)
-    iAuIntro. iApply (aacc_aupd_abort with "AU"); first done.
+    iApply (aacc_aupd_abort with "AU"); first done.
     iIntros (x) "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
-    iIntros "$ !> AU !> _".
+    iIntros "$ !> AU !>".
     (* Now go on *)
-    wp_apply cas_spec; [done|iAccu|].
+    awp_apply cas_spec; first done.
     (* Prove the atomic update for CAS *)
-    iAuIntro. iApply (aacc_aupd with "AU"); first done.
+    iApply (aacc_aupd with "AU"); first done.
     iIntros (x') "H↦". iAaccIntro with "H↦"; first by eauto with iFrame.
     iIntros "H↦ !>".
     destruct (decide (#x' = #x)) as [[= ->]|Hx].
-    - iRight. iFrame. iIntros "HΦ !> _".
+    - iRight. iFrame. iIntros "HΦ !>".
       wp_if. by iApply "HΦ".
-    - iLeft. iFrame. iIntros "AU !> _".
+    - iLeft. iFrame. iIntros "AU !>".
       wp_if. iApply "IH". done.
   Qed.
 
@@ -116,17 +116,17 @@ Section increment.
       weak_incr #l @ ⊤
     <<< ⌜v = v'⌝ ∗ l ↦ #(v + 1), RET #v >>>.
   Proof.
-    iIntros "Hl". iApply wp_atomic_intro. iIntros (Φ) "AU". wp_lam.
+    iIntros "Hl" (Φ) "AU". wp_lam.
     wp_apply (atomic_wp_seq $! (load_spec _) with "Hl").
-    iIntros "Hl". wp_apply store_spec; first by iAccu.
+    iIntros "Hl". awp_apply store_spec.
     (* Prove the atomic update for store *)
-    iAuIntro. iApply (aacc_aupd_commit with "AU"); first done.
+    iApply (aacc_aupd_commit with "AU"); first done.
     iIntros (x) "H↦".
     iDestruct (mapsto_agree with "Hl H↦") as %[= <-].
     iCombine "Hl" "H↦" as "Hl". iAaccIntro with "Hl".
     { iIntros "[$ $]"; eauto. }
     iIntros "$ !>". iSplit; first done.
-    iIntros "HΦ !> _". wp_seq. done.
+    iIntros "HΦ !>". wp_seq. done.
   Qed.
 
 End increment.
@@ -149,8 +149,8 @@ Section increment_client.
     (* FIXME: I am only using persistent stuff, so I should be allowed
        to move this to the persisten context even without the additional â–¡. *)
     iAssert (â–¡ WP incr #l {{ _, True }})%I as "#Aupd".
-    { iAlways. wp_apply incr_spec; first by iAccu. clear x.
-      iAuIntro. iInv nroot as (x) ">H↦". iAaccIntro with "H↦"; first by eauto 10.
+    { iAlways. awp_apply incr_spec. clear x.
+      iInv nroot as (x) ">H↦". iAaccIntro with "H↦"; first by eauto 10.
       iIntros "H↦ !>". iSplitL "H↦"; first by eauto 10.
       (* The continuation: From after the atomic triple to the postcondition of the WP *)
       done.
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 05eb1b56e759f5c1c5c787e33212a2640711f028..92851e21392ece4904ec055e61f96694d512e84e 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -1,4 +1,5 @@
 From iris.program_logic Require Export weakestpre total_weakestpre.
+From iris.program_logic Require Import atomic.
 From iris.proofmode Require Import coq_tactics reduction.
 From iris.proofmode Require Export tactics.
 From iris.heap_lang Require Export tactics lifting.
@@ -354,24 +355,40 @@ Proof.
 Qed.
 End heap.
 
-Tactic Notation "wp_apply" open_constr(lem) :=
+(** Evaluate [lem] to a hypothesis [H] that can be applied, and then run
+[wp_bind K; tac H] for every possible evaluation context.  [tac] can do
+[iApplyHyp H] to actually apply the hypothesis.  TC resolution of [lem] premises
+happens *after* [tac H] got executed. *)
+Tactic Notation "wp_apply_core" open_constr(lem) tactic(tac) :=
   wp_pures;
   iPoseProofCore lem as false true (fun H =>
     lazymatch goal with
     | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
       reshape_expr e ltac:(fun K e' =>
-        wp_bind_core K; iApplyHyp H; try iNext; try wp_expr_simpl) ||
+        wp_bind_core K; tac H) ||
       lazymatch iTypeOf H with
       | Some (_,?P) => fail "wp_apply: cannot apply" P
       end
     | |- envs_entails _ (twp ?s ?E ?e ?Q) =>
       reshape_expr e ltac:(fun K e' =>
-        twp_bind_core K; iApplyHyp H; try wp_expr_simpl) ||
+        twp_bind_core K; tac H) ||
       lazymatch iTypeOf H with
       | Some (_,?P) => fail "wp_apply: cannot apply" P
       end
     | _ => fail "wp_apply: not a 'wp'"
     end).
+Tactic Notation "wp_apply" open_constr(lem) :=
+  wp_apply_core lem (fun H => iApplyHyp H; try iNext; try wp_expr_simpl).
+(** Tactic tailored for atomic triples: the first, simple one just runs
+[iAuIntro] on the goal, as atomic triples always have an atomic update as their
+premise.  The second one additionaly does some framing: it gets rid of [Hs] from
+the context, which is intended to be the non-laterable assertions that iAuIntro
+would choke on.  You get them all back in the continuation of the atomic
+operation. *)
+Tactic Notation "awp_apply" open_constr(lem) :=
+  wp_apply_core lem (fun H => iApplyHyp H; last iAuIntro).
+Tactic Notation "awp_apply" open_constr(lem) "without" constr(Hs) :=
+  wp_apply_core lem (fun H => iApply wp_frame_wand_l; iSplitL Hs; [iAccu|iApplyHyp H; last iAuIntro]).
 
 Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
   let Htmp := iFresh in
diff --git a/theories/program_logic/atomic.v b/theories/program_logic/atomic.v
index 9c0df10983a554c10c2b9b16c4c756827cdbca3d..25df772be33d0ef798f62fb779f4a33050d1a96c 100644
--- a/theories/program_logic/atomic.v
+++ b/theories/program_logic/atomic.v
@@ -14,8 +14,8 @@ Definition atomic_wp `{irisG Λ Σ} {TA TB : tele}
   (β: TA → TB → iProp Σ) (* atomic post-condition *)
   (f: TA → TB → val Λ) (* Turn the return data into the return value *)
   : iProp Σ :=
-    (∀ Q (Φ : val Λ → iProp Σ), Q -∗
-             atomic_update Eo ∅ α β (λ.. x y, Q -∗ Φ (f x y)) -∗
+    (∀ (Φ : val Λ → iProp Σ),
+             atomic_update Eo ∅ α β (λ.. x y, Φ (f x y)) -∗
              WP e {{ Φ }})%I.
 (* Note: To add a private postcondition, use
    atomic_update α β Eo Ei (λ x y, POST x y -∗ Φ (f x y)) *)
@@ -102,8 +102,8 @@ Section lemmas.
     atomic_wp e Eo α β f -∗
     ∀ Φ, ∀.. x, α x -∗ (∀.. y, β x y -∗ Φ (f x y)) -∗ WP e {{ Φ }}.
   Proof.
-    rewrite ->tforall_forall in HL.
-    iIntros "Hwp" (Φ x) "Hα HΦ". iApply ("Hwp" with "[HΦ]"); first iAccu.
+    rewrite ->tforall_forall in HL. iIntros "Hwp" (Φ x) "Hα HΦ".
+    iApply wp_frame_wand_l. iSplitL "HΦ"; first iAccu. iApply "Hwp".
     iAuIntro. iAaccIntro with "Hα"; first by eauto. iIntros (y) "Hβ !>".
     (* FIXME: Using ssreflect rewrite does not work, see Coq bug #7773. *)
     rewrite ->!tele_app_bind. iIntros "HΦ". iApply "HΦ". done.
@@ -116,23 +116,12 @@ Section lemmas.
     (∀ Φ, ∀.. x, α x -∗ (∀.. y, β x y -∗ Φ (f x y)) -∗ WP e {{ Φ }}) -∗
     atomic_wp e Eo α β f.
   Proof.
-    simpl in HP. iIntros "Hwp" (Q Φ) "HQ HΦ". iApply fupd_wp.
+    simpl in HP. iIntros "Hwp" (Φ) "HΦ". iApply fupd_wp.
     iMod ("HΦ") as "[#Hα [Hclose _]]". iMod ("Hclose" with "Hα") as "HΦ".
     iApply wp_fupd. iApply ("Hwp" with "Hα"). iIntros "!>" (y) "Hβ".
     iMod ("HΦ") as "[_ [_ Hclose]]". iMod ("Hclose" with "Hβ") as "HΦ".
     (* FIXME: Using ssreflect rewrite does not work, see Coq bug #7773. *)
-    rewrite ->!tele_app_bind. iApply "HΦ". done.
+    rewrite ->!tele_app_bind. done.
   Qed.
 
-  (* Way to prove an atomic triple without seeing the Q *)
-  Lemma wp_atomic_intro e Eo α β f :
-    (∀ (Φ : val Λ → iProp),
-             atomic_update Eo ∅ α β (λ.. x y, Φ (f x y)) -∗
-             WP e {{ Φ }}) -∗
-    atomic_wp e Eo α β f.
-  Proof.
-    iIntros "Hwp" (Q Φ) "HQ AU". iApply (wp_wand with "[-HQ]").
-    { iApply ("Hwp" $! (λ v, Q -∗ Φ v)%I). done. }
-    iIntros (v) "HΦ". iApply "HΦ". done.
-  Qed.
 End lemmas.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 92ddffd1616eac02a9e906c36d9fbe860695fdbe..65513253b663208b17b632dbc092cc29273903ad 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -241,6 +241,13 @@ Proof. iIntros "[H Hwp]". iApply (wp_wand with "Hwp H"). Qed.
 Lemma wp_wand_r s E e Φ Ψ :
   WP e @ s; E {{ Φ }} ∗ (∀ v, Φ v -∗ Ψ v) ⊢ WP e @ s; E {{ Ψ }}.
 Proof. iIntros "[Hwp H]". iApply (wp_wand with "Hwp H"). Qed.
+Lemma wp_frame_wand_l s E e Q Φ :
+  Q ∗ WP e @ s; E {{ v, Q -∗ Φ v }} -∗ WP e @ s; E {{ Φ }}.
+Proof.
+  iIntros "[HQ HWP]". iApply (wp_wand with "HWP").
+  iIntros (v) "HΦ". by iApply "HΦ".
+Qed.
+
 End wp.
 
 (** Proofmode class instances *)
diff --git a/theories/proofmode/class_instances_bi.v b/theories/proofmode/class_instances_bi.v
index cc13f1972e98195cd51eb052ae3fb039e91276fc..b4c2bf994098f9e66d4d67c884db37c70f20fe9e 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
@@ -591,6 +591,11 @@ Proof.
   apply wand_elim_l', big_sepL2_app.
 Qed.
 
+Global Instance from_and_big_sepMS_union_persistent `{Countable A} (Φ : A → PROP) X1 X2 :
+  (∀ y, Persistent (Φ y)) →
+  FromAnd ([∗ mset] y ∈ X1 ∪ X2, Φ y) ([∗ mset] y ∈ X1, Φ y) ([∗ mset] y ∈ X2, Φ y).
+Proof. intros. by rewrite /FromAnd big_sepMS_union persistent_and_sep_1. Qed.
+
 (** FromSep *)
 Global Instance from_sep_sep P1 P2 : FromSep (P1 ∗ P2) P1 P2 | 100.
 Proof. by rewrite /FromSep. Qed.
@@ -644,6 +649,10 @@ Global Instance from_sep_big_sepL2_app {A B} (Φ : nat → A → B → PROP)
     ([∗ list] k ↦ y1;y2 ∈ l1'';l2'', Φ (length l1' + k) y1 y2).
 Proof. rewrite /IsApp=>-> ->. apply wand_elim_l', big_sepL2_app. Qed.
 
+Global Instance from_sep_big_sepMS_union `{Countable A} (Φ : A → PROP) X1 X2 :
+  FromSep ([∗ mset] y ∈ X1 ∪ X2, Φ y) ([∗ mset] y ∈ X1, Φ y) ([∗ mset] y ∈ X2, Φ y).
+Proof. by rewrite /FromSep big_sepMS_union. Qed.
+
 Global Instance from_sep_bupd `{BiBUpd PROP} P Q1 Q2 :
   FromSep P Q1 Q2 → FromSep (|==> P) (|==> Q1) (|==> Q2).
 Proof. rewrite /FromSep=><-. apply bupd_sep. Qed.
@@ -793,6 +802,10 @@ Global Instance into_sep_big_sepL2_cons {A B}
     (Φ 0 x1 x2) ([∗ list] k ↦ y1;y2 ∈ l1';l2', Φ (S k) y1 y2).
 Proof. rewrite /IsCons=>-> ->. by rewrite /IntoSep big_sepL2_cons. Qed.
 
+Global Instance into_sep_big_sepMS_union `{Countable A} (Φ : A → PROP) X1 X2 :
+  IntoSep ([∗ mset] y ∈ X1 ∪ X2, Φ y) ([∗ mset] y ∈ X1, Φ y) ([∗ mset] y ∈ X2, Φ y).
+Proof. by rewrite /IntoSep big_sepMS_union. Qed.
+
 (** FromOr *)
 Global Instance from_or_or P1 P2 : FromOr (P1 ∨ P2) P1 P2.
 Proof. by rewrite /FromOr. Qed.
diff --git a/theories/proofmode/frame_instances.v b/theories/proofmode/frame_instances.v
index 3dee777bfa9cbfb8c15a6ac6587e29da4bd42b1e..9a5c852043f724e7caba86485f5c055416f6680e 100644
--- a/theories/proofmode/frame_instances.v
+++ b/theories/proofmode/frame_instances.v
@@ -105,6 +105,11 @@ Global Instance frame_big_sepL2_app {A B} p (Φ : nat → A → B → PROP)
   Frame p R ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2) Q.
 Proof. rewrite /IsApp /Frame=>-> -> ->. apply wand_elim_l', big_sepL2_app. Qed.
 
+Global Instance frame_big_sepMS_union `{Countable A} p (Φ : A → PROP) R Q X1 X2 :
+  Frame p R (([∗ mset] y ∈ X1, Φ y) ∗ [∗ mset] y ∈ X2, Φ y) Q →
+  Frame p R ([∗ mset] y ∈ X1 ∪ X2, Φ y) Q.
+Proof. by rewrite /Frame big_sepMS_union. Qed.
+
 Global Instance make_and_true_l P : KnownLMakeAnd True P P.
 Proof. apply left_id, _. Qed.
 Global Instance make_and_true_r P : KnownRMakeAnd P True P.