From 7453ecb0b86e50d98d6c2952c7d0ae731351740c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 29 Nov 2017 16:51:46 +0100
Subject: [PATCH] =?UTF-8?q?Rename=20`wp=5Fsimpl`=20=E2=86=92=20`wp=5Fexpr?=
 =?UTF-8?q?=5Fsimpl`=20to=20emphasize=20that=20it=20only=20simplifies=20th?=
 =?UTF-8?q?e=20expression=20part.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/heap_lang/proofmode.v | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 67814c975..7c7489035 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -5,17 +5,17 @@ From iris.heap_lang Require Export tactics lifting.
 Set Default Proof Using "Type".
 Import uPred.
 
-Lemma tac_wp_simpl `{heapG Σ} Δ E Φ e e' :
+Lemma tac_wp_expr_eval `{heapG Σ} Δ E Φ e e' :
   e = e' →
   envs_entails Δ (WP e' @ E {{ Φ }}) → envs_entails Δ (WP e @ E {{ Φ }}).
 Proof. by intros ->. Qed.
 
-Ltac wp_eval t :=
+Ltac wp_expr_eval t :=
   try iStartProof;
-  try (eapply tac_wp_simpl; [t; reflexivity|]).
+  try (eapply tac_wp_expr_eval; [t; reflexivity|]).
 
-Ltac wp_simpl := wp_eval simpl.
-Ltac wp_simpl_subst := wp_eval simpl_subst.
+Ltac wp_expr_simpl := wp_expr_eval simpl.
+Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst.
 
 Lemma tac_wp_pure `{heapG Σ} Δ Δ' E e1 e2 φ Φ :
   PureExec φ e1 e2 →
@@ -46,7 +46,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
       [apply _                        (* PureExec *)
       |try fast_done                  (* The pure condition for PureExec *)
       |apply _                        (* IntoLaters *)
-      |wp_simpl_subst; try wp_value_head (* new goal *)
+      |wp_expr_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'"
@@ -168,7 +168,7 @@ Tactic Notation "wp_apply" open_constr(lem) :=
     lazymatch goal with
     | |- envs_entails _ (wp ?E ?e ?Q) =>
       reshape_expr e ltac:(fun K e' =>
-        wp_bind_core K; iApplyHyp H; try iNext; wp_simpl) ||
+        wp_bind_core K; iApplyHyp H; try iNext; wp_expr_simpl) ||
       lazymatch iTypeOf H with
       | Some (_,?P) => fail "wp_apply: cannot apply" P
       end
@@ -187,7 +187,7 @@ Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
     |first [intros l | fail 1 "wp_alloc:" l "not fresh"];
       eexists; split;
         [env_cbv; reflexivity || fail "wp_alloc:" H "not fresh"
-        |wp_simpl; try wp_value_head]]
+        |wp_expr_simpl; try wp_value_head]]
   | _ => fail "wp_alloc: not a 'wp'"
   end.
 
@@ -204,7 +204,7 @@ Tactic Notation "wp_load" :=
     [apply _
     |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
      iAssumptionCore || fail "wp_load: cannot find" l "↦ ?"
-    |wp_simpl; try wp_value_head]
+    |wp_expr_simpl; try wp_value_head]
   | _ => fail "wp_load: not a 'wp'"
   end.
 
@@ -220,7 +220,7 @@ Tactic Notation "wp_store" :=
     |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
      iAssumptionCore || fail "wp_store: cannot find" l "↦ ?"
     |env_cbv; reflexivity
-    |wp_simpl; try first [wp_pure (Seq (Lit LitUnit) _)|wp_value_head]]
+    |wp_expr_simpl; try first [wp_pure (Seq (Lit LitUnit) _)|wp_value_head]]
   | _ => fail "wp_store: not a 'wp'"
   end.
 
@@ -236,7 +236,7 @@ Tactic Notation "wp_cas_fail" :=
     |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
      iAssumptionCore || fail "wp_cas_fail: cannot find" l "↦ ?"
     |try congruence
-    |wp_simpl; try wp_value_head]
+    |wp_expr_simpl; try wp_value_head]
   | _ => fail "wp_cas_fail: not a 'wp'"
   end.
 
@@ -253,6 +253,6 @@ Tactic Notation "wp_cas_suc" :=
      iAssumptionCore || fail "wp_cas_suc: cannot find" l "↦ ?"
     |try congruence
     |env_cbv; reflexivity
-    |wp_simpl; try wp_value_head]
+    |wp_expr_simpl; try wp_value_head]
   | _ => fail "wp_cas_suc: not a 'wp'"
   end.
-- 
GitLab