diff --git a/theories/bi/lib/atomic.v b/theories/bi/lib/atomic.v
index 59df84626c95f725c2a6e0afd0dc56e49c16a8ea..906de8a56c0641154a5787569217fc087884b10c 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 9d5a5bc665788c8a5f67e5feb98721238715312c..52591bf6e220e0b977c2ecb7c1c1572a0d431d4b 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 a1e363e75e2f72d9bae6c97c36c5b6557f82f948..8aff6e52bad42f10c71266ba5c9f79ce52181ade 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 d13067c9b8c6cbb81743d1d7f0158cdef7c093c9..51ccf1ead67fc20848f6e6d328cc3395777dae2f 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
 ].