From 97f7dfb312273acd63d1ece9f8ce604cbdb79949 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 24 Jan 2019 21:14:25 +0100
Subject: [PATCH] test awp_apply without

---
 tests/atomic.8.8.ref                | 14 ++++++++++++++
 tests/atomic.v                      | 15 ++++++++++++++-
 theories/program_logic/weakestpre.v |  2 +-
 3 files changed, 29 insertions(+), 2 deletions(-)

diff --git a/tests/atomic.8.8.ref b/tests/atomic.8.8.ref
index 72d993e6e..a3f918527 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
diff --git a/tests/atomic.v b/tests/atomic.v
index 000566884..236ec1e71 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 Σ}.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index e9e83a10b..f46b92465 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -246,7 +246,7 @@ Lemma wp_frame_wand_l s E e Q Φ :
 Proof.
   iIntros "[HQ HWP]". iApply (wp_wand with "HWP").
   iIntros (v) "HΦ". by iApply "HΦ".
-Qed. 
+Qed.
 
 End wp.
 
-- 
GitLab