From c25f4d65328cb74bb5331af32ff5b9246540bb3a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 12 Sep 2018 11:50:07 +0200
Subject: [PATCH] =?UTF-8?q?Rename=20`prop=5Fof=5Fenv`=20=E2=86=92=20`env?=
 =?UTF-8?q?=5Fto=5Fprop`?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

All the `env` operations are prefixed `env_`, so this is more consistent.
---
 theories/bi/lib/atomic.v          | 4 ++--
 theories/proofmode/coq_tactics.v  | 4 ++--
 theories/proofmode/environments.v | 4 ++--
 theories/proofmode/reduction.v    | 2 +-
 4 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/theories/bi/lib/atomic.v b/theories/bi/lib/atomic.v
index 59df84626..906de8a56 100644
--- a/theories/bi/lib/atomic.v
+++ b/theories/bi/lib/atomic.v
@@ -431,12 +431,12 @@ Section proof_mode.
   Lemma tac_aupd_intro Γp Γs n α β Eo Ei Φ P :
     Timeless (PROP:=PROP) emp →
     TCForall Laterable (env_to_list Γs) →
-    P = prop_of_env Γs →
+    P = env_to_prop Γs →
     envs_entails (Envs Γp Γs n) (atomic_acc Eo Ei α P β Φ) →
     envs_entails (Envs Γp Γs n) (atomic_update Eo Ei α β Φ).
   Proof.
     intros ? HΓs ->. rewrite envs_entails_eq of_envs_eq' /atomic_acc /=.
-    setoid_rewrite prop_of_env_sound =>HAU.
+    setoid_rewrite env_to_prop_sound =>HAU.
     apply aupd_intro; [apply _..|]. done.
   Qed.
 End proof_mode.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 9d5a5bc66..52591bf6e 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -601,11 +601,11 @@ Qed.
 
 (** * Accumulate hypotheses *)
 Lemma tac_accu Δ P :
-  prop_of_env (env_spatial Δ) = P →
+  env_to_prop (env_spatial Δ) = P →
   envs_entails Δ P.
 Proof.
   rewrite envs_entails_eq=><-.
-  rewrite prop_of_env_sound /of_envs and_elim_r sep_elim_r //.
+  rewrite env_to_prop_sound /of_envs and_elim_r sep_elim_r //.
 Qed.
 
 (** * Fresh *)
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index a1e363e75..8aff6e52b 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -335,7 +335,7 @@ Definition envs_split {PROP} (d : direction)
   ''(Δ1,Δ2) ← envs_split_go js Δ (envs_clear_spatial Δ);
   if d is Right then Some (Δ1,Δ2) else Some (Δ2,Δ1).
 
-Definition prop_of_env {PROP : bi} (Γ : env PROP) : PROP :=
+Definition env_to_prop {PROP : bi} (Γ : env PROP) : PROP :=
   let fix aux Γ acc :=
     match Γ with Enil => acc | Esnoc Γ _ P => aux Γ (P ∗ acc)%I end
   in
@@ -659,7 +659,7 @@ Proof.
   destruct d; simplify_eq/=; solve_sep_entails.
 Qed.
 
-Lemma prop_of_env_sound Γ : prop_of_env Γ ⊣⊢ [∗] Γ.
+Lemma env_to_prop_sound Γ : env_to_prop Γ ⊣⊢ [∗] Γ.
 Proof.
   destruct Γ as [|Γ ? P]; simpl; first done.
   revert P. induction Γ as [|Γ IH ? Q]=>P; simpl.
diff --git a/theories/proofmode/reduction.v b/theories/proofmode/reduction.v
index d13067c9b..51ccf1ead 100644
--- a/theories/proofmode/reduction.v
+++ b/theories/proofmode/reduction.v
@@ -13,7 +13,7 @@ Declare Reduction pm_eval := cbv [
   envs_lookup envs_lookup_delete envs_delete envs_snoc envs_app
   envs_simple_replace envs_replace envs_split
   envs_clear_spatial envs_clear_persistent envs_incr_counter
-  envs_split_go envs_split prop_of_env
+  envs_split_go envs_split env_to_prop
   (* PM option combinators *)
   pm_option_bind pm_from_option pm_option_fun
 ].
-- 
GitLab