From a0edf35dea7a7f1c9e774d2dec368667811df3e9 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 4 Jul 2018 23:45:55 +0200
Subject: [PATCH] use iDestructHyp instead of iDestruct
---
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 fe8a81c37..3ca89589e 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -365,7 +365,7 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
first [intros l | fail 1 "wp_alloc:" l "not fresh"];
eexists; split;
[pm_reflexivity || fail "wp_alloc:" H "not fresh"
- |iDestruct Htmp as H; wp_expr_simpl; try wp_value_head] in
+ |iDestructHyp Htmp as H; wp_expr_simpl; try wp_value_head] in
iStartProof;
lazymatch goal with
| |- envs_entails _ (wp ?s ?E ?e ?Q) =>
--
GitLab