From 133d10e0ea89c2fa394cb98510b3fa03d644995d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 24 Nov 2017 14:44:10 +0100
Subject: [PATCH] Move `simpl` arround to make stuff work.
---
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 7c374b4c5..e868107d5 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -24,12 +24,12 @@ Proof. rewrite /envs_entails=> ? ->. by apply wp_value. Qed.
Ltac wp_value_head := eapply tac_wp_value; [apply _|lazy beta].
Tactic Notation "wp_pure" open_constr(efoc) :=
- iStartProof;
+ iStartProof; simpl; (* simpl possible [of_val]s *)
lazymatch goal with
| |- envs_entails _ (wp ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
unify e' efoc;
- eapply tac_wp_pure;
- [simpl; change e with (fill K e'); apply _ (* PureExec *)
+ eapply (tac_wp_pure _ _ _ (fill K e'));
+ [apply _ (* PureExec *)
|try fast_done (* The pure condition for PureExec *)
|apply _ (* IntoLaters *)
|simpl_subst; try wp_value_head (* new goal *)
--
GitLab