From 1fb1b2c77872e0250ede607e440b6b8e7934f55b Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Thu, 21 Sep 2017 09:37:31 +0200
Subject: [PATCH] Reorder the assumptions for `tac_wp_pure`

This way `IntoLaterNEnvs` is ought to be computed less frequently
---
 theories/heap_lang/proofmode.v | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 1e0b9823f..bcfe13343 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -40,9 +40,9 @@ Ltac wp_pure_done :=
   end.
 
 Lemma tac_wp_pure `{heapG Σ} K Δ Δ' E e1 e2 φ Φ :
-  IntoLaterNEnvs 1 Δ Δ' →
   PureExec φ e1 e2 →
   φ →
+  IntoLaterNEnvs 1 Δ Δ' →
   (Δ' ⊢ WP fill K e2 @ E {{ Φ }}) →
   (Δ ⊢ WP fill K e1 @ E {{ Φ }}).
 Proof.
@@ -55,12 +55,11 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
   iStartProof;
   lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
-    let e'' := eval hnf in e' in
-    unify e'' efoc;
+    unify e' efoc;
     eapply (tac_wp_pure K);
-    [apply _                  (* IntoLaters *)
-    |unlock; simpl; apply _   (* PureExec *)
+    [unlock; simpl; apply _   (* PureExec *)
     |wp_pure_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'"
-- 
GitLab