From a8054b66d345e003cbb87010336ff6716aae1d37 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 8 Jan 2020 13:20:25 +0100
Subject: [PATCH] fix ltac parsing
---
theories/heap_lang/proofmode.v | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 95ae906c1..a31e6f7e2 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -408,7 +408,7 @@ End heap.
[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) :=
+Tactic Notation "wp_apply_core" open_constr(lem) tactic3(tac) :=
wp_pures;
iPoseProofCore lem as false (fun H =>
lazymatch goal with
@@ -435,10 +435,10 @@ 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));
+ 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]));
+ 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) :=
--
GitLab