From 3a5c5045e7c762238014bdc794c3186c83e1a571 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 25 Sep 2017 20:23:57 +0200
Subject: [PATCH] Move some stuff.

---
 theories/heap_lang/proofmode.v | 17 ++++++++---------
 1 file changed, 8 insertions(+), 9 deletions(-)

diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index a9d2d5f3a..5801ae991 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -5,15 +5,6 @@ From iris.heap_lang Require Export tactics lifting.
 Set Default Proof Using "Type".
 Import uPred.
 
-(** wp-specific helper tactics *)
-Ltac wp_bind_core K :=
-  lazymatch eval hnf in K with
-  | [] => idtac
-  | _ => etrans; [|fast_by apply (wp_bind K)]; simpl
-  end.
-
-Ltac wp_value_head := etrans; [|eapply wp_value; apply _]; simpl.
-
 Lemma tac_wp_pure `{heapG Σ} K Δ Δ' E e1 e2 φ Φ :
   PureExec φ e1 e2 →
   φ →
@@ -26,6 +17,8 @@ Proof.
   by rewrite -ectx_lifting.wp_ectx_bind_inv.
 Qed.
 
+Ltac wp_value_head := etrans; [|eapply wp_value; apply _]; simpl.
+
 Tactic Notation "wp_pure" open_constr(efoc) :=
   iStartProof;
   lazymatch goal with
@@ -54,6 +47,12 @@ Tactic Notation "wp_proj" := wp_pure (Fst _) || wp_pure (Snd _).
 Tactic Notation "wp_case" := wp_pure (Case _ _ _).
 Tactic Notation "wp_match" := wp_case; wp_let.
 
+Ltac wp_bind_core K :=
+  lazymatch eval hnf in K with
+  | [] => idtac
+  | _ => etrans; [|fast_by apply (wp_bind K)]; simpl
+  end.
+
 Tactic Notation "wp_bind" open_constr(efoc) :=
   iStartProof;
   lazymatch goal with
-- 
GitLab