From b4d7c4efcec368414fb305e21736cb6049921b84 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 24 Nov 2017 15:26:39 +0100
Subject: [PATCH] Only run `simpl` locally.
---
theories/heap_lang/proofmode.v | 20 +++++++++++---------
1 file changed, 11 insertions(+), 9 deletions(-)
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index e868107d5..8263ff881 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -24,16 +24,18 @@ 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; simpl; (* simpl possible [of_val]s *)
+ iStartProof;
lazymatch goal with
- | |- envs_entails _ (wp ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
- unify e' efoc;
- 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 *)
- ])
+ | |- envs_entails _ (wp ?E ?e ?Q) =>
+ let e := eval simpl in e in
+ reshape_expr e ltac:(fun K e' =>
+ unify e' efoc;
+ 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 *)
+ ])
|| fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a reduct"
| _ => fail "wp_pure: not a 'wp'"
end.
--
GitLab