From 71d78026a9286e16fd757c7803aa4720150645a8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 5 Nov 2017 14:20:49 +0100
Subject: [PATCH] Small simplification to `wp_bind_core`.

---
 theories/heap_lang/proofmode.v | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 8a047e571..677aa6063 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -66,10 +66,9 @@ Ltac wp_bind_core K :=
 Tactic Notation "wp_bind" open_constr(efoc) :=
   iStartProof;
   lazymatch goal with
-  | |- envs_entails _ (wp ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
-    match e' with
-    | efoc => unify e' efoc; wp_bind_core K
-    end) || fail "wp_bind: cannot find" efoc "in" e
+  | |- envs_entails _ (wp ?E ?e ?Q) =>
+    reshape_expr e ltac:(fun K e' => unify e' efoc; wp_bind_core K)
+    || fail "wp_bind: cannot find" efoc "in" e
   | _ => fail "wp_bind: not a 'wp'"
   end.
 
-- 
GitLab