From f8ef60fe5fc74995d09c215c9ed06fb5145c20bf Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 31 Dec 2017 17:55:36 +0100
Subject: [PATCH] Make `wp_expr_eval` a `Tactic Notation` so that the argument
 is parsed as a 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 dac198480..c63f1ec69 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -10,7 +10,7 @@ Lemma tac_wp_expr_eval `{heapG Σ} Δ s E Φ e e' :
   envs_entails Δ (WP e' @ s; E {{ Φ }}) → envs_entails Δ (WP e @ s; E {{ Φ }}).
 Proof. by intros ->. Qed.
 
-Ltac wp_expr_eval t :=
+Tactic Notation "wp_expr_eval" tactic(t) :=
   try iStartProof;
   try (eapply tac_wp_expr_eval; [t; reflexivity|]).
 
-- 
GitLab