From 4d52d19564dbc849a7995863ceff2d1b2f3d7877 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 9 Jan 2020 10:06:34 +0100
Subject: [PATCH] fix the last remaining tactic()

---
 theories/heap_lang/proofmode.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index a31e6f7e2..d1632a886 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -16,7 +16,7 @@ Lemma tac_twp_expr_eval `{!heapG Σ} Δ s E Φ e e' :
   envs_entails Δ (WP e' @ s; E [{ Φ }]) → envs_entails Δ (WP e @ s; E [{ Φ }]).
 Proof. by intros ->. Qed.
 
-Tactic Notation "wp_expr_eval" tactic(t) :=
+Tactic Notation "wp_expr_eval" tactic3(t) :=
   iStartProof;
   lazymatch goal with
   | |- envs_entails _ (wp ?s ?E ?e ?Q) =>
-- 
GitLab