From a15dc76f957c96bd67ac8a28064ab5f77e871a39 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 4 Jan 2021 22:55:38 +0100
Subject: [PATCH] Put heap_lang tactics in better order.

---
 iris_heap_lang/proofmode.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index 6bf7a0fe0..a640e92d1 100644
--- a/iris_heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -26,6 +26,7 @@ Tactic Notation "wp_expr_eval" tactic3(t) :=
       [let x := fresh in intros x; t; unfold x; notypeclasses refine eq_refl|]
   | _ => fail "wp_expr_eval: not a 'wp'"
   end.
+Ltac wp_expr_simpl := wp_expr_eval simpl.
 
 Lemma tac_wp_pure `{!heapG Σ} Δ Δ' s E K e1 e2 φ n Φ :
   PureExec φ n e1 e2 →
@@ -65,8 +66,6 @@ Lemma tac_twp_value `{!heapG Σ} Δ s E (Φ : val → iPropI Σ) v :
   envs_entails Δ (|={E}=> Φ v) → envs_entails Δ (WP (Val v) @ s; E [{ Φ }]).
 Proof. rewrite envs_entails_eq=> ->. by rewrite twp_value_fupd. Qed.
 
-Ltac wp_expr_simpl := wp_expr_eval simpl.
-
 (** Simplify the goal if it is [WP] of a value.
   If the postcondition already allows a fupd, do not add a second one.
   But otherwise, *do* add a fupd. This ensures that all the lemmas applied
-- 
GitLab