From d3556db237095ee6017077ff42bf387a04cc4db2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 8 Jan 2020 13:12:07 +0100
Subject: [PATCH] fix awp_apply error message

---
 tests/atomic.ref               | 5 +----
 tests/atomic.v                 | 2 +-
 theories/heap_lang/proofmode.v | 6 ++++--
 3 files changed, 6 insertions(+), 7 deletions(-)

diff --git a/tests/atomic.ref b/tests/atomic.ref
index 7146b97ea..ba5c5ad60 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -17,10 +17,7 @@
 The command has indeed failed with message:
 Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 The command has indeed failed with message:
-Tactic failure: wp_apply: cannot apply
-(<<< ∀ (v : val) (q : Qp), ?Goal ↦{q} v >>>
-   ! #?Goal @ ⊤
- <<< ?Goal ↦{q} v, RET v >>>).
+Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 "printing"
      : string
 1 subgoal
diff --git a/tests/atomic.v b/tests/atomic.v
index 4e69316d0..125a261c1 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -30,7 +30,7 @@ Section error.
   Restart.
     iIntros "HP". Fail awp_apply load_spec.
   Abort.
-End error.  
+End error.
 
 
 (* Test if AWP and the AU obtained from AWP print. *)
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index fc4913c1b..95ae906c1 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -435,9 +435,11 @@ 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).
+  (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]).
+  (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
-- 
GitLab