From 599493de20b18d2cf64bc6168ab75f0d2814880c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 13 May 2022 10:07:55 +0200
Subject: [PATCH] No longer make `envs_entails_unseal` local.

---
 iris/bi/lib/atomic.v          |   2 +-
 iris/proofmode/coq_tactics.v  | 118 +++++++++++++++++-----------------
 iris/proofmode/environments.v |   2 +-
 iris/proofmode/ltac_tactics.v |  14 ++--
 iris_heap_lang/proofmode.v    |  56 ++++++++--------
 tests/heapprop.v              |   2 +-
 6 files changed, 97 insertions(+), 97 deletions(-)

diff --git a/iris/bi/lib/atomic.v b/iris/bi/lib/atomic.v
index d9eef2930..7b65aa8ef 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -462,7 +462,7 @@ Section proof_mode.
     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 environments.envs_entails_unseal of_envs_eq' /atomic_acc /=.
+    intros ? HΓs ->. rewrite envs_entails_unseal of_envs_eq' /atomic_acc /=.
     setoid_rewrite env_to_prop_sound =>HAU.
     apply aupd_intro; [apply _..|]. done.
   Qed.
diff --git a/iris/proofmode/coq_tactics.v b/iris/proofmode/coq_tactics.v
index 117714f66..4dd269b4a 100644
--- a/iris/proofmode/coq_tactics.v
+++ b/iris/proofmode/coq_tactics.v
@@ -16,7 +16,7 @@ Implicit Types P Q : PROP.
 (** * Starting and stopping the proof mode *)
 Lemma tac_start P : envs_entails (Envs Enil Enil 1) P → ⊢ P.
 Proof.
-  rewrite environments.envs_entails_unseal !of_envs_eq /=.
+  rewrite envs_entails_unseal !of_envs_eq /=.
   rewrite intuitionistically_True_emp left_id=><-.
   apply and_intro=> //. apply pure_intro; repeat constructor.
 Qed.
@@ -29,7 +29,7 @@ Lemma tac_stop Δ P :
    end ⊢ P) →
   envs_entails Δ P.
 Proof.
-  rewrite environments.envs_entails_unseal !of_envs_eq. intros <-.
+  rewrite envs_entails_unseal !of_envs_eq. intros <-.
   rewrite and_elim_r -env_to_prop_and_sound -env_to_prop_sound.
   destruct (env_intuitionistic Δ), (env_spatial Δ);
     by rewrite /= ?intuitionistically_True_emp ?left_id ?right_id.
@@ -53,7 +53,7 @@ Lemma tac_eval_in Δ i p P P' Q :
   envs_entails Δ Q.
 Proof.
   destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
-  rewrite environments.envs_entails_unseal /=. intros ? HP ?.
+  rewrite envs_entails_unseal /=. intros ? HP ?.
   rewrite envs_simple_replace_singleton_sound //; simpl.
   by rewrite HP wand_elim_r.
 Qed.
@@ -74,7 +74,7 @@ Local Instance affine_env_spatial Δ :
 Proof. intros H. induction H; simpl; apply _. Qed.
 
 Lemma tac_emp_intro Δ : AffineEnv (env_spatial Δ) → envs_entails Δ emp.
-Proof. intros. by rewrite environments.envs_entails_unseal (affine (of_envs Δ)). Qed.
+Proof. intros. by rewrite envs_entails_unseal (affine (of_envs Δ)). Qed.
 
 Lemma tac_assumption Δ i p P Q :
   envs_lookup i Δ = Some (p,P) →
@@ -84,7 +84,7 @@ Lemma tac_assumption Δ i p P Q :
    else TCOr (Absorbing Q) (AffineEnv (env_spatial Δ'))) →
   envs_entails Δ Q.
 Proof.
-  intros ?? H. rewrite environments.envs_entails_unseal envs_lookup_sound //.
+  intros ?? H. rewrite envs_entails_unseal envs_lookup_sound //.
   simpl in *. destruct (env_spatial_is_nil _) eqn:?.
   - by rewrite (env_spatial_is_nil_intuitionistically _) // sep_elim_l.
   - rewrite from_assumption. destruct H; by rewrite sep_elim_l.
@@ -98,7 +98,7 @@ Lemma tac_assumption_coq Δ P Q :
   envs_entails Δ Q.
 Proof.
   rewrite /FromAssumption /bi_emp_valid /= => HP HPQ H.
-  rewrite environments.envs_entails_unseal -(left_id emp%I bi_sep (of_envs Δ)).
+  rewrite envs_entails_unseal -(left_id emp%I bi_sep (of_envs Δ)).
   rewrite -bi.intuitionistically_emp HP HPQ.
   destruct (env_spatial_is_nil _) eqn:?.
   - by rewrite (env_spatial_is_nil_intuitionistically _) // sep_elim_l.
@@ -114,7 +114,7 @@ Lemma tac_rename Δ i j p P Q :
   envs_entails Δ Q.
 Proof.
   destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
-  rewrite environments.envs_entails_unseal=> ??. rewrite envs_simple_replace_singleton_sound //.
+  rewrite envs_entails_unseal=> ??. rewrite envs_simple_replace_singleton_sound //.
   by rewrite wand_elim_r.
 Qed.
 
@@ -124,20 +124,20 @@ Lemma tac_clear Δ i p P Q :
   envs_entails (envs_delete true i p Δ) Q →
   envs_entails Δ Q.
 Proof.
-  rewrite environments.envs_entails_unseal=> ?? HQ. rewrite envs_lookup_sound //. rewrite HQ.
+  rewrite envs_entails_unseal=> ?? HQ. rewrite envs_lookup_sound //. rewrite HQ.
   by destruct p; rewrite /= sep_elim_r.
 Qed.
 
 (** * False *)
 Lemma tac_ex_falso Δ Q : envs_entails Δ False → envs_entails Δ Q.
-Proof. by rewrite environments.envs_entails_unseal -(False_elim Q). Qed.
+Proof. by rewrite envs_entails_unseal -(False_elim Q). Qed.
 
 Lemma tac_false_destruct Δ i p P Q :
   envs_lookup i Δ = Some (p,P) →
   P = False%I →
   envs_entails Δ Q.
 Proof.
-  rewrite environments.envs_entails_unseal => ??. subst. rewrite envs_lookup_sound //; simpl.
+  rewrite envs_entails_unseal => ??. subst. rewrite envs_lookup_sound //; simpl.
   by rewrite intuitionistically_if_elim sep_elim_l False_elim.
 Qed.
 
@@ -148,7 +148,7 @@ Lemma tac_pure_intro Δ Q φ a :
   φ →
   envs_entails Δ Q.
 Proof.
-  intros ???. rewrite environments.envs_entails_unseal -(from_pure a Q). destruct a; simpl.
+  intros ???. rewrite envs_entails_unseal -(from_pure a Q). destruct a; simpl.
   - by rewrite (affine (of_envs Δ)) pure_True // affinely_True_emp affinely_emp.
   - by apply pure_intro.
 Qed.
@@ -159,7 +159,7 @@ Lemma tac_pure Δ i p P φ Q :
   (if p then TCTrue else TCOr (Affine P) (Absorbing Q)) →
   (φ → envs_entails (envs_delete true i p Δ) Q) → envs_entails Δ Q.
 Proof.
-  rewrite environments.envs_entails_unseal=> ?? HPQ HQ.
+  rewrite envs_entails_unseal=> ?? HPQ HQ.
   rewrite envs_lookup_sound //; simpl. destruct p; simpl.
   - rewrite (into_pure P) -persistently_and_intuitionistically_sep_l persistently_pure.
     by apply pure_elim_l.
@@ -175,7 +175,7 @@ Lemma tac_pure_revert Δ φ P Q :
   envs_entails Δ (P -∗ Q) →
   (φ → envs_entails Δ Q).
 Proof.
-  rewrite /FromAffinely environments.envs_entails_unseal. intros <- -> ?.
+  rewrite /FromAffinely envs_entails_unseal. intros <- -> ?.
   by rewrite pure_True // affinely_True_emp affinely_emp left_id.
 Qed.
 
@@ -191,7 +191,7 @@ Lemma tac_intuitionistic Δ i j p P P' Q :
   envs_entails Δ Q.
 Proof.
   destruct (envs_replace _ _ _ _ _) as [Δ'|] eqn:Hrep; last done.
-  rewrite environments.envs_entails_unseal=>?? HPQ HQ. rewrite envs_replace_singleton_sound //=.
+  rewrite envs_entails_unseal=>?? HPQ HQ. rewrite envs_replace_singleton_sound //=.
   destruct p; simpl; rewrite /bi_intuitionistically.
   - by rewrite -(into_persistent true P) /= wand_elim_r.
   - destruct HPQ.
@@ -212,7 +212,7 @@ Lemma tac_spatial Δ i j p P P' Q :
   envs_entails Δ Q.
 Proof.
   intros ? HP. destruct (envs_replace _ _ _ _ _) as [Δ'|] eqn:Hrep; last done.
-  rewrite environments.envs_entails_unseal=> <-. rewrite envs_replace_singleton_sound //; simpl.
+  rewrite envs_entails_unseal=> <-. rewrite envs_replace_singleton_sound //; simpl.
   destruct p; simpl; last destruct HP.
   - by rewrite intuitionistically_affinely (from_affinely P' P) wand_elim_r.
   - by rewrite wand_elim_r.
@@ -230,7 +230,7 @@ Lemma tac_impl_intro Δ i P P' Q R :
   envs_entails Δ R.
 Proof.
   destruct (envs_app _ _ _) eqn:?; last done.
-  rewrite /FromImpl environments.envs_entails_unseal => <- ???. destruct (env_spatial_is_nil Δ) eqn:?.
+  rewrite /FromImpl envs_entails_unseal => <- ???. destruct (env_spatial_is_nil Δ) eqn:?.
   - rewrite (env_spatial_is_nil_intuitionistically Δ) //; simpl. apply impl_intro_l.
     rewrite envs_app_singleton_sound //; simpl.
     rewrite -(from_affinely P' P) -affinely_and_lr.
@@ -248,7 +248,7 @@ Lemma tac_impl_intro_intuitionistic Δ i P P' Q R :
   envs_entails Δ R.
 Proof.
   destruct (envs_app _ _ _) eqn:?; last done.
-  rewrite /FromImpl environments.envs_entails_unseal => <- ??.
+  rewrite /FromImpl envs_entails_unseal => <- ??.
   rewrite envs_app_singleton_sound //=. apply impl_intro_l.
   rewrite (_ : P = <pers>?false P)%I // (into_persistent false P).
   by rewrite persistently_and_intuitionistically_sep_l wand_elim_r.
@@ -256,7 +256,7 @@ Qed.
 Lemma tac_impl_intro_drop Δ P Q R :
   FromImpl R P Q → envs_entails Δ Q → envs_entails Δ R.
 Proof.
-  rewrite /FromImpl environments.envs_entails_unseal => <- ?. apply impl_intro_l. by rewrite and_elim_r.
+  rewrite /FromImpl envs_entails_unseal => <- ?. apply impl_intro_l. by rewrite and_elim_r.
 Qed.
 
 Lemma tac_wand_intro Δ i P Q R :
@@ -268,7 +268,7 @@ Lemma tac_wand_intro Δ i P Q R :
   envs_entails Δ R.
 Proof.
   destruct (envs_app _ _ _) as [Δ'|] eqn:Hrep; last done.
-  rewrite /FromWand environments.envs_entails_unseal => <- HQ.
+  rewrite /FromWand envs_entails_unseal => <- HQ.
   rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
 Qed.
 
@@ -283,7 +283,7 @@ Lemma tac_wand_intro_intuitionistic Δ i P P' Q R :
   envs_entails Δ R.
 Proof.
   destruct (envs_app _ _ _) as [Δ'|] eqn:Hrep; last done.
-  rewrite /FromWand environments.envs_entails_unseal => <- ? HPQ HQ.
+  rewrite /FromWand envs_entails_unseal => <- ? HPQ HQ.
   rewrite envs_app_singleton_sound //=. apply wand_intro_l. destruct HPQ.
   - rewrite -(affine_affinely P) (_ : P = <pers>?false P)%I //
             (into_persistent _ P) wand_elim_r //.
@@ -297,7 +297,7 @@ Lemma tac_wand_intro_drop Δ P Q R :
   envs_entails Δ Q →
   envs_entails Δ R.
 Proof.
-  rewrite environments.envs_entails_unseal /FromWand => <- HPQ ->. apply wand_intro_l. by rewrite sep_elim_r.
+  rewrite envs_entails_unseal /FromWand => <- HPQ ->. apply wand_intro_l. by rewrite sep_elim_r.
 Qed.
 
 (* This is pretty much [tac_specialize_assert] with [js:=[j]] and [tac_exact],
@@ -312,7 +312,7 @@ Lemma tac_specialize remove_intuitionistic Δ i p j q P1 P2 R Q :
   | None => False
   end → envs_entails Δ Q.
 Proof.
-  rewrite environments.envs_entails_unseal /IntoWand. intros ?? HR ?.
+  rewrite envs_entails_unseal /IntoWand. intros ?? HR ?.
   destruct (envs_replace _ _ _ _ _) as [Δ''|] eqn:?; last done.
   rewrite (envs_lookup_sound' _ remove_intuitionistic) //.
   rewrite envs_replace_singleton_sound //. destruct p; simpl in *.
@@ -338,7 +338,7 @@ Lemma tac_specialize_assert Δ j (q am neg : bool) js R P1 P2 P1' Q :
   | None => False
   end → envs_entails Δ Q.
 Proof.
-  rewrite environments.envs_entails_unseal. intros ?? Hmod HQ.
+  rewrite envs_entails_unseal. intros ?? Hmod HQ.
   destruct (_ ≫= _) as [[Δ1 Δ2']|] eqn:?; last done.
   destruct HQ as [HP1 HQ].
   destruct (envs_split _ _ _) as [[? Δ2]|] eqn:?; simplify_eq/=;
@@ -356,9 +356,9 @@ Proof.
 Qed.
 
 Lemma tac_unlock_emp Δ Q : envs_entails Δ Q → envs_entails Δ (emp ∗ locked Q).
-Proof. rewrite environments.envs_entails_unseal=> ->. by rewrite -lock left_id. Qed.
+Proof. rewrite envs_entails_unseal=> ->. by rewrite -lock left_id. Qed.
 Lemma tac_unlock_True Δ Q : envs_entails Δ Q → envs_entails Δ (True ∗ locked Q).
-Proof. rewrite environments.envs_entails_unseal=> ->. by rewrite -lock -True_sep_2. Qed.
+Proof. rewrite envs_entails_unseal=> ->. by rewrite -lock -True_sep_2. Qed.
 Lemma tac_unlock Δ Q : envs_entails Δ Q → envs_entails Δ (locked Q).
 Proof. by unlock. Qed.
 
@@ -370,7 +370,7 @@ Lemma tac_specialize_frame Δ j (q am : bool) R P1 P2 P1' Q Q' :
   Q' = (P2 -∗ Q)%I →
   envs_entails Δ Q.
 Proof.
-  rewrite environments.envs_entails_unseal. intros ?? Hmod HPQ ->.
+  rewrite envs_entails_unseal. intros ?? Hmod HPQ ->.
   rewrite envs_lookup_sound //. rewrite HPQ -lock.
   rewrite (into_wand q false) /= assoc -(comm _ P1') -assoc wand_trans.
   destruct am; [done|destruct Hmod]. by rewrite wand_elim_r.
@@ -388,7 +388,7 @@ Lemma tac_specialize_assert_pure Δ j q a R P1 P2 φ Q :
   envs_entails Δ Q.
 Proof.
   destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:?; last done.
-  rewrite environments.envs_entails_unseal=> ?????. rewrite envs_simple_replace_singleton_sound //=.
+  rewrite envs_entails_unseal=> ?????. rewrite envs_simple_replace_singleton_sound //=.
   rewrite -intuitionistically_if_idemp (into_wand q true) /=.
   rewrite -(from_pure a P1) pure_True //.
   rewrite -affinely_affinely_if affinely_True_emp affinely_emp.
@@ -406,7 +406,7 @@ Lemma tac_specialize_assert_intuitionistic Δ j q P1 P1' P2 R Q :
   | None => False
   end → envs_entails Δ Q.
 Proof.
-  rewrite environments.envs_entails_unseal => ???? HP1 HQ.
+  rewrite envs_entails_unseal => ???? HP1 HQ.
   destruct (envs_simple_replace _ _ _ _) as [Δ''|] eqn:?; last done.
   rewrite -HQ envs_lookup_sound //.
   rewrite -(idemp bi_and (of_envs (envs_delete _ _ _ _))).
@@ -428,7 +428,7 @@ Lemma tac_specialize_intuitionistic_helper Δ j q P R R' Q :
   | None => False
   end → envs_entails Δ Q.
 Proof.
-  rewrite environments.envs_entails_unseal => ?? HR ??.
+  rewrite envs_entails_unseal => ?? HR ??.
   destruct (envs_replace _ _ _ _ _) as [Δ'|] eqn:?; last done.
   rewrite -(idemp bi_and (of_envs Δ)) {1}HR.
   rewrite envs_replace_singleton_sound //; destruct q; simpl.
@@ -446,7 +446,7 @@ Lemma tac_specialize_intuitionistic_helper_done Δ i q P :
   envs_lookup i Δ = Some (q,P) →
   envs_entails Δ (<absorb> P).
 Proof.
-  rewrite environments.envs_entails_unseal /bi_absorbingly=> /envs_lookup_sound=> ->.
+  rewrite envs_entails_unseal /bi_absorbingly=> /envs_lookup_sound=> ->.
   rewrite intuitionistically_if_elim comm. f_equiv; auto using pure_intro.
 Qed.
 
@@ -457,7 +457,7 @@ Lemma tac_revert Δ i Q :
   end →
   envs_entails Δ Q.
 Proof.
-  rewrite environments.envs_entails_unseal => HQ.
+  rewrite envs_entails_unseal => HQ.
   destruct (envs_lookup_delete _ _ _) as [[[p P] Δ']|] eqn:?; last done.
   rewrite envs_lookup_delete_sound //=.
   rewrite HQ. destruct p; simpl; auto using wand_elim_r.
@@ -466,7 +466,7 @@ Qed.
 Class IntoIH (φ : Prop) (Δ : envs PROP) (Q : PROP) :=
   into_ih : φ → □ of_envs Δ ⊢ Q.
 Global Instance into_ih_entails Δ Q : IntoIH (envs_entails Δ Q) Δ Q.
-Proof. by rewrite environments.envs_entails_unseal /IntoIH bi.intuitionistically_elim. Qed.
+Proof. by rewrite envs_entails_unseal /IntoIH bi.intuitionistically_elim. Qed.
 Global Instance into_ih_forall {A} (φ : A → Prop) Δ Φ :
   (∀ x, IntoIH (φ x) Δ (Φ x)) → IntoIH (∀ x, φ x) Δ (∀ x, Φ x) | 2.
 Proof. rewrite /IntoIH=> HΔ ?. apply forall_intro=> x. by rewrite (HΔ x). Qed.
@@ -516,7 +516,7 @@ Lemma tac_revert_ih Δ P Q {φ : Prop} (Hφ : φ) :
   envs_entails Δ (<pers> P → Q) →
   envs_entails Δ Q.
 Proof.
-  rewrite /IntoIH environments.envs_entails_unseal. intros HP ? HPQ.
+  rewrite /IntoIH envs_entails_unseal. intros HP ? HPQ.
   rewrite (env_spatial_is_nil_intuitionistically Δ) //.
   rewrite -(idemp bi_and (□ (of_envs Δ))%I).
   rewrite -{1}intuitionistically_idemp {1}intuitionistically_into_persistently_1.
@@ -530,7 +530,7 @@ Lemma tac_assert Δ j P Q :
   end → envs_entails Δ Q.
 Proof.
   destruct (envs_app _ _ _) as [Δ'|] eqn:?; last done.
-  rewrite environments.envs_entails_unseal=> ?. rewrite (envs_app_singleton_sound Δ) //; simpl.
+  rewrite envs_entails_unseal=> ?. rewrite (envs_app_singleton_sound Δ) //; simpl.
   by rewrite -(entails_wand P) // intuitionistically_emp emp_wand.
 Qed.
 
@@ -565,7 +565,7 @@ Lemma tac_pose_proof Δ j P Q :
   envs_entails Δ Q.
 Proof.
   destruct (envs_app _ _ _) as [Δ'|] eqn:?; last done.
-  rewrite environments.envs_entails_unseal => HP <-. rewrite envs_app_singleton_sound //=.
+  rewrite envs_entails_unseal => HP <-. rewrite envs_app_singleton_sound //=.
   by rewrite -HP /= intuitionistically_emp emp_wand.
 Qed.
 
@@ -582,7 +582,7 @@ Lemma tac_pose_proof_hyp Δ i j Q :
 Proof.
   destruct (envs_lookup_delete _ _ _) as [((p&P)&Δ')|] eqn:Hlookup; last done.
   destruct (envs_app _ _ _) as [Δ''|] eqn:?; last done.
-  rewrite environments.envs_entails_unseal. move: Hlookup. rewrite envs_lookup_delete_Some.
+  rewrite envs_entails_unseal. move: Hlookup. rewrite envs_lookup_delete_Some.
   intros [? ->] <-.
   rewrite envs_lookup_sound' // envs_app_singleton_sound //=.
   by rewrite wand_elim_r.
@@ -593,14 +593,14 @@ Lemma tac_apply Δ i p R P1 P2 :
   IntoWand p false R P1 P2 →
   envs_entails (envs_delete true i p Δ) P1 → envs_entails Δ P2.
 Proof.
-  rewrite environments.envs_entails_unseal => ?? HP1. rewrite envs_lookup_sound //.
+  rewrite envs_entails_unseal => ?? HP1. rewrite envs_lookup_sound //.
   by rewrite (into_wand p false) /= HP1 wand_elim_l.
 Qed.
 
 (** * Conjunction splitting *)
 Lemma tac_and_split Δ P Q1 Q2 :
   FromAnd P Q1 Q2 → envs_entails Δ Q1 → envs_entails Δ Q2 → envs_entails Δ P.
-Proof. rewrite environments.envs_entails_unseal. intros. rewrite -(from_and P). by apply and_intro. Qed.
+Proof. rewrite envs_entails_unseal. intros. rewrite -(from_and P). by apply and_intro. Qed.
 
 (** * Separating conjunction splitting *)
 Lemma tac_sep_split Δ d js P Q1 Q2 :
@@ -611,7 +611,7 @@ Lemma tac_sep_split Δ d js P Q1 Q2 :
   end → envs_entails Δ P.
 Proof.
   destruct (envs_split _ _ _) as [(Δ1&Δ2)|] eqn:?; last done.
-  rewrite environments.envs_entails_unseal=>? [HQ1 HQ2].
+  rewrite envs_entails_unseal=>? [HQ1 HQ2].
   rewrite envs_split_sound //. by rewrite HQ1 HQ2.
 Qed.
 
@@ -635,7 +635,7 @@ Lemma tac_combine Δ1 Δ2 Δ3 js p Ps j P Q :
   envs_app p (Esnoc Enil j P) Δ2 = Some Δ3 →
   envs_entails Δ3 Q → envs_entails Δ1 Q.
 Proof.
-  rewrite environments.envs_entails_unseal => ??? <-. rewrite envs_lookup_delete_list_sound //.
+  rewrite envs_entails_unseal => ??? <-. rewrite envs_lookup_delete_list_sound //.
   rewrite from_seps. rewrite envs_app_singleton_sound //=.
   by rewrite wand_elim_r.
 Qed.
@@ -651,7 +651,7 @@ Lemma tac_and_destruct Δ i p j1 j2 P P1 P2 Q :
   envs_entails Δ Q.
 Proof.
   destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
-  rewrite environments.envs_entails_unseal. intros. rewrite envs_simple_replace_sound //=. destruct p.
+  rewrite envs_entails_unseal. intros. rewrite envs_simple_replace_sound //=. destruct p.
   - by rewrite (into_and _ P) /= right_id -(comm _ P1) wand_elim_r.
   - by rewrite /= (into_sep P) right_id -(comm _ P1) wand_elim_r.
 Qed.
@@ -671,7 +671,7 @@ Lemma tac_and_destruct_choice Δ i p d j P P1 P2 Q :
   end → envs_entails Δ Q.
 Proof.
   destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
-  rewrite environments.envs_entails_unseal => ? HP HQ.
+  rewrite envs_entails_unseal => ? HP HQ.
   rewrite envs_simple_replace_singleton_sound //=. destruct p.
   { rewrite (into_and _ P) HQ. destruct d; simpl.
     - by rewrite and_elim_l wand_elim_r.
@@ -689,7 +689,7 @@ Qed.
 Lemma tac_frame_pure Δ (φ : Prop) P Q :
   φ → Frame true ⌜φ⌝ P Q → envs_entails Δ Q → envs_entails Δ P.
 Proof.
-  rewrite environments.envs_entails_unseal => ? Hframe ->. rewrite -Hframe /=.
+  rewrite envs_entails_unseal => ? Hframe ->. rewrite -Hframe /=.
   rewrite -persistently_and_intuitionistically_sep_l persistently_pure.
   auto using and_intro, pure_intro.
 Qed.
@@ -699,7 +699,7 @@ Lemma tac_frame Δ i p R P Q :
   Frame p R P Q →
   envs_entails (envs_delete false i p Δ) Q → envs_entails Δ P.
 Proof.
-  rewrite environments.envs_entails_unseal. intros ? Hframe HQ.
+  rewrite envs_entails_unseal. intros ? Hframe HQ.
   rewrite (envs_lookup_sound' _ false) //. by rewrite -Hframe HQ.
 Qed.
 
@@ -707,12 +707,12 @@ Qed.
 Lemma tac_or_l Δ P Q1 Q2 :
   FromOr P Q1 Q2 → envs_entails Δ Q1 → envs_entails Δ P.
 Proof.
-  rewrite environments.envs_entails_unseal=> ? ->. rewrite -(from_or P). by apply or_intro_l'.
+  rewrite envs_entails_unseal=> ? ->. rewrite -(from_or P). by apply or_intro_l'.
 Qed.
 Lemma tac_or_r Δ P Q1 Q2 :
   FromOr P Q1 Q2 → envs_entails Δ Q2 → envs_entails Δ P.
 Proof.
-  rewrite environments.envs_entails_unseal=> ? ->. rewrite -(from_or P). by apply or_intro_r'.
+  rewrite envs_entails_unseal=> ? ->. rewrite -(from_or P). by apply or_intro_r'.
 Qed.
 
 Lemma tac_or_destruct Δ i p j1 j2 P P1 P2 Q :
@@ -726,7 +726,7 @@ Lemma tac_or_destruct Δ i p j1 j2 P P1 P2 Q :
 Proof.
   destruct (envs_simple_replace i p (Esnoc Enil j1 P1)) as [Δ1|] eqn:?; last done.
   destruct (envs_simple_replace i p (Esnoc Enil j2 P2)) as [Δ2|] eqn:?; last done.
-  rewrite environments.envs_entails_unseal. intros ?? (HP1&HP2). rewrite envs_lookup_sound //.
+  rewrite envs_entails_unseal. intros ?? (HP1&HP2). rewrite envs_lookup_sound //.
   rewrite (into_or P) intuitionistically_if_or sep_or_r; apply or_elim.
   - rewrite (envs_simple_replace_singleton_sound' _ Δ1) //.
     by rewrite wand_elim_r.
@@ -741,7 +741,7 @@ Lemma tac_forall_intro {A} Δ (Φ : A → PROP) Q name :
    let _ := name in
    ∀ a, envs_entails Δ (Φ a)) →
   envs_entails Δ Q.
-Proof. rewrite environments.envs_entails_unseal /FromForall=> <-. apply forall_intro. Qed.
+Proof. rewrite envs_entails_unseal /FromForall=> <-. apply forall_intro. Qed.
 
 Lemma tac_forall_specialize {A} Δ i p P (Φ : A → PROP) Q :
   envs_lookup i Δ = Some (p, P) → IntoForall P Φ →
@@ -752,7 +752,7 @@ Lemma tac_forall_specialize {A} Δ i p P (Φ : A → PROP) Q :
       end) →
   envs_entails Δ Q.
 Proof.
-  rewrite environments.envs_entails_unseal. intros ?? (x&?).
+  rewrite envs_entails_unseal. intros ?? (x&?).
   destruct (envs_simple_replace) as [Δ'|] eqn:?; last done.
   rewrite envs_simple_replace_singleton_sound //; simpl.
   by rewrite (into_forall P) (forall_elim x) wand_elim_r.
@@ -760,13 +760,13 @@ Qed.
 
 Lemma tac_forall_revert {A} Δ (Φ : A → PROP) :
   envs_entails Δ (∀ a, Φ a) → ∀ a, envs_entails Δ (Φ a).
-Proof. rewrite environments.envs_entails_unseal => HΔ a. by rewrite HΔ (forall_elim a). Qed.
+Proof. rewrite envs_entails_unseal => HΔ a. by rewrite HΔ (forall_elim a). Qed.
 
 (** * Existential *)
 Lemma tac_exist {A} Δ P (Φ : A → PROP) :
   FromExist P Φ → (∃ a, envs_entails Δ (Φ a)) → envs_entails Δ P.
 Proof.
-  rewrite environments.envs_entails_unseal => ? [a ?].
+  rewrite envs_entails_unseal => ? [a ?].
   rewrite -(from_exist P). eauto using exist_intro'.
 Qed.
 
@@ -783,7 +783,7 @@ Lemma tac_exist_destruct {A} Δ i p j P (Φ : A → PROP) (name: ident_name) Q :
      end) →
   envs_entails Δ Q.
 Proof.
-  rewrite environments.envs_entails_unseal => ?? HΦ. rewrite envs_lookup_sound //.
+  rewrite envs_entails_unseal => ?? HΦ. rewrite envs_lookup_sound //.
   rewrite (into_exist P) intuitionistically_if_exist sep_exist_r.
   apply exist_elim=> a; specialize (HΦ a) as Hmatch.
   destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:Hrep; last done.
@@ -802,7 +802,7 @@ Lemma tac_modal_elim Δ i j p p' φ P' P Q Q' :
   envs_entails Δ Q.
 Proof.
   destruct (envs_replace _ _ _ _ _) as [Δ'|] eqn:?; last done.
-  rewrite environments.envs_entails_unseal => ??? HΔ. rewrite envs_replace_singleton_sound //=.
+  rewrite envs_entails_unseal => ??? HΔ. rewrite envs_replace_singleton_sound //=.
   rewrite HΔ. by eapply elim_modal.
 Qed.
 
@@ -811,7 +811,7 @@ Lemma tac_accu Δ P :
   env_to_prop (env_spatial Δ) = P →
   envs_entails Δ P.
 Proof.
-  rewrite environments.envs_entails_unseal=><-.
+  rewrite envs_entails_unseal=><-.
   rewrite env_to_prop_sound !of_envs_eq and_elim_r sep_elim_r //.
 Qed.
 
@@ -830,7 +830,7 @@ Lemma tac_inv_elim {X : Type} Δ i j φ p Pinv Pin Pout (Pclose : option (X →
     with Some Δ'' => envs_entails Δ'' R | None => False end) →
   envs_entails Δ Q.
 Proof.
-  rewrite environments.envs_entails_unseal=> ? Hinv ? /(_ Q) Hmatch.
+  rewrite envs_entails_unseal=> ? Hinv ? /(_ Q) Hmatch.
   destruct (envs_app _ _ _) eqn:?; last done.
   rewrite -Hmatch (envs_lookup_sound' _ false) // envs_app_singleton_sound //; simpl.
   apply wand_elim_r', wand_mono; last done. apply wand_intro_r, wand_intro_r.
@@ -848,7 +848,7 @@ Lemma tac_rewrite `{!BiInternalEq PROP} Δ i p Pxy d Q :
     NonExpansive Φ →
     envs_entails Δ (Φ (if d is Left then x else y)) → envs_entails Δ Q.
 Proof.
-  intros ? A x y ? HPxy -> ?. rewrite environments.envs_entails_unseal.
+  intros ? A x y ? HPxy -> ?. rewrite envs_entails_unseal.
   apply internal_eq_rewrite'; auto. rewrite {1}envs_lookup_sound //.
   rewrite (into_internal_eq Pxy x y) intuitionistically_if_elim sep_elim_l.
   destruct d; auto using internal_eq_sym.
@@ -867,7 +867,7 @@ Lemma tac_rewrite_in `{!BiInternalEq PROP} Δ i p Pxy j q P d Q :
     end →
     envs_entails Δ Q.
 Proof.
-  rewrite environments.envs_entails_unseal /IntoInternalEq => ?? A x y Φ HPxy HP ? Hentails.
+  rewrite envs_entails_unseal /IntoInternalEq => ?? A x y Φ HPxy HP ? Hentails.
   destruct (envs_simple_replace _ _ _ _) as [Δ'|] eqn:?; last done. rewrite -Hentails.
   rewrite -(idemp bi_and (of_envs Δ)) {2}(envs_lookup_sound _ i) //.
   rewrite (envs_simple_replace_singleton_sound _ _ j) //=.
@@ -890,7 +890,7 @@ Lemma tac_löb Δ i Q :
   envs_entails Δ Q.
 Proof.
   destruct (envs_app _ _ _) as [Δ'|] eqn:?; last done.
-  rewrite environments.envs_entails_unseal => ?? HQ.
+  rewrite envs_entails_unseal => ?? HQ.
   rewrite (env_spatial_is_nil_intuitionistically Δ) //.
   rewrite envs_app_singleton_sound //; simpl. rewrite HQ.
   apply löb_wand_intuitionistically.
@@ -1080,7 +1080,7 @@ Section tac_modal_intro.
     φ →
     envs_entails (Envs Γp' Γs' n) Q → envs_entails (Envs Γp Γs n) Q'.
   Proof.
-    rewrite environments.envs_entails_unseal /FromModal !of_envs_eq => HQ' HΓp HΓs ? Hφ HQ.
+    rewrite envs_entails_unseal /FromModal !of_envs_eq => HQ' HΓp HΓs ? Hφ HQ.
     apply pure_elim_l=> -[???]. assert (envs_wf (Envs Γp' Γs' n)) as Hwf.
     { split; simpl in *.
       - destruct HΓp as [| |????? []| |]; eauto using Enil_wf.
diff --git a/iris/proofmode/environments.v b/iris/proofmode/environments.v
index 9931c6e9a..126286e4a 100644
--- a/iris/proofmode/environments.v
+++ b/iris/proofmode/environments.v
@@ -266,7 +266,7 @@ Local Definition pre_envs_entails_unseal :
 
 Definition envs_entails {PROP : bi} (Δ : envs PROP) (Q : PROP) : Prop :=
   pre_envs_entails  PROP (env_intuitionistic Δ) (env_spatial Δ) Q.
-Local Definition envs_entails_unseal :
+Definition envs_entails_unseal :
   @envs_entails = λ PROP (Δ : envs PROP) Q, (of_envs Δ ⊢ Q).
 Proof. by rewrite /envs_entails pre_envs_entails_unseal. Qed.
 Global Arguments envs_entails {PROP} Δ Q%I.
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 661d731b3..e574cb04d 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -3426,19 +3426,19 @@ Global Hint Extern 0 (envs_entails _ emp) => iEmpIntro : core.
 (* TODO: look for a more principled way of adding trivial hints like those
 below; see the discussion in !75 for further details. *)
 Global Hint Extern 0 (envs_entails _ (_ ≡ _)) =>
-  rewrite environments.envs_entails_unseal; apply internal_eq_refl : core.
+  rewrite envs_entails_unseal; apply internal_eq_refl : core.
 Global Hint Extern 0 (envs_entails _ (big_opL _ _ _)) =>
-  rewrite environments.envs_entails_unseal; apply (big_sepL_nil' _) : core.
+  rewrite envs_entails_unseal; apply (big_sepL_nil' _) : core.
 Global Hint Extern 0 (envs_entails _ (big_sepL2 _ _ _)) =>
-  rewrite environments.envs_entails_unseal; apply (big_sepL2_nil' _) : core.
+  rewrite envs_entails_unseal; apply (big_sepL2_nil' _) : core.
 Global Hint Extern 0 (envs_entails _ (big_opM _ _ _)) =>
-  rewrite environments.envs_entails_unseal; apply (big_sepM_empty' _) : core.
+  rewrite envs_entails_unseal; apply (big_sepM_empty' _) : core.
 Global Hint Extern 0 (envs_entails _ (big_sepM2 _ _ _)) =>
-  rewrite environments.envs_entails_unseal; apply (big_sepM2_empty' _) : core.
+  rewrite envs_entails_unseal; apply (big_sepM2_empty' _) : core.
 Global Hint Extern 0 (envs_entails _ (big_opS _ _ _)) =>
-  rewrite environments.envs_entails_unseal; apply (big_sepS_empty' _) : core.
+  rewrite envs_entails_unseal; apply (big_sepS_empty' _) : core.
 Global Hint Extern 0 (envs_entails _ (big_opMS _ _ _)) =>
-  rewrite environments.envs_entails_unseal; apply (big_sepMS_empty' _) : core.
+  rewrite envs_entails_unseal; apply (big_sepMS_empty' _) : core.
 
 (* These introduce as much as possible at once, for better performance. *)
 Global Hint Extern 0 (envs_entails _ (∀ _, _)) => iIntros : core.
diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index db3b63009..a4e1dc21f 100644
--- a/iris_heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -35,7 +35,7 @@ Lemma tac_wp_pure `{!heapGS Σ} Δ Δ' s E K e1 e2 φ n Φ :
   envs_entails Δ' (WP (fill K e2) @ s; E {{ Φ }}) →
   envs_entails Δ (WP (fill K e1) @ s; E {{ Φ }}).
 Proof.
-  rewrite environments.envs_entails_unseal=> ??? HΔ'. rewrite into_laterN_env_sound /=.
+  rewrite envs_entails_unseal=> ??? HΔ'. rewrite into_laterN_env_sound /=.
   (* We want [pure_exec_fill] to be available to TC search locally. *)
   pose proof @pure_exec_fill.
   rewrite HΔ' -lifting.wp_pure_step_later //.
@@ -46,7 +46,7 @@ Lemma tac_twp_pure `{!heapGS Σ} Δ s E K e1 e2 φ n Φ :
   envs_entails Δ (WP (fill K e2) @ s; E [{ Φ }]) →
   envs_entails Δ (WP (fill K e1) @ s; E [{ Φ }]).
 Proof.
-  rewrite environments.envs_entails_unseal=> ?? ->.
+  rewrite envs_entails_unseal=> ?? ->.
   (* We want [pure_exec_fill] to be available to TC search locally. *)
   pose proof @pure_exec_fill.
   rewrite -total_lifting.twp_pure_step //.
@@ -54,17 +54,17 @@ Qed.
 
 Lemma tac_wp_value_nofupd `{!heapGS Σ} Δ s E Φ v :
   envs_entails Δ (Φ v) → envs_entails Δ (WP (Val v) @ s; E {{ Φ }}).
-Proof. rewrite environments.envs_entails_unseal=> ->. by apply wp_value. Qed.
+Proof. rewrite envs_entails_unseal=> ->. by apply wp_value. Qed.
 Lemma tac_twp_value_nofupd `{!heapGS Σ} Δ s E Φ v :
   envs_entails Δ (Φ v) → envs_entails Δ (WP (Val v) @ s; E [{ Φ }]).
-Proof. rewrite environments.envs_entails_unseal=> ->. by apply twp_value. Qed.
+Proof. rewrite envs_entails_unseal=> ->. by apply twp_value. Qed.
 
 Lemma tac_wp_value `{!heapGS Σ} Δ s E (Φ : val → iPropI Σ) v :
   envs_entails Δ (|={E}=> Φ v) → envs_entails Δ (WP (Val v) @ s; E {{ Φ }}).
-Proof. rewrite environments.envs_entails_unseal=> ->. by rewrite wp_value_fupd. Qed.
+Proof. rewrite envs_entails_unseal=> ->. by rewrite wp_value_fupd. Qed.
 Lemma tac_twp_value `{!heapGS Σ} Δ s E (Φ : val → iPropI Σ) v :
   envs_entails Δ (|={E}=> Φ v) → envs_entails Δ (WP (Val v) @ s; E [{ Φ }]).
-Proof. rewrite environments.envs_entails_unseal=> ->. by rewrite twp_value_fupd. Qed.
+Proof. rewrite envs_entails_unseal=> ->. by rewrite twp_value_fupd. Qed.
 
 (** Simplify the goal if it is [WP] of a value.
   If the postcondition already allows a fupd, do not add a second one.
@@ -174,12 +174,12 @@ Lemma tac_wp_bind `{!heapGS Σ} K Δ s E Φ e f :
   f = (λ e, fill K e) → (* as an eta expanded hypothesis so that we can `simpl` it *)
   envs_entails Δ (WP e @ s; E {{ v, WP f (Val v) @ s; E {{ Φ }} }})%I →
   envs_entails Δ (WP fill K e @ s; E {{ Φ }}).
-Proof. rewrite environments.envs_entails_unseal=> -> ->. by apply: wp_bind. Qed.
+Proof. rewrite envs_entails_unseal=> -> ->. by apply: wp_bind. Qed.
 Lemma tac_twp_bind `{!heapGS Σ} K Δ s E Φ e f :
   f = (λ e, fill K e) → (* as an eta expanded hypothesis so that we can `simpl` it *)
   envs_entails Δ (WP e @ s; E [{ v, WP f (Val v) @ s; E [{ Φ }] }])%I →
   envs_entails Δ (WP fill K e @ s; E [{ Φ }]).
-Proof. rewrite environments.envs_entails_unseal=> -> ->. by apply: twp_bind. Qed.
+Proof. rewrite envs_entails_unseal=> -> ->. by apply: twp_bind. Qed.
 
 Ltac wp_bind_core K :=
   lazymatch eval hnf in K with
@@ -224,7 +224,7 @@ Lemma tac_wp_allocN Δ Δ' s E j K v n Φ :
     end) →
   envs_entails Δ (WP fill K (AllocN (Val $ LitV $ LitInt n) (Val v)) @ s; E {{ Φ }}).
 Proof.
-  rewrite environments.envs_entails_unseal=> ? ? HΔ.
+  rewrite envs_entails_unseal=> ? ? HΔ.
   rewrite -wp_bind. eapply wand_apply; first exact: wp_allocN.
   rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
   specialize (HΔ l).
@@ -242,7 +242,7 @@ Lemma tac_twp_allocN Δ s E j K v n Φ :
     end) →
   envs_entails Δ (WP fill K (AllocN (Val $ LitV $ LitInt n) (Val v)) @ s; E [{ Φ }]).
 Proof.
-  rewrite environments.envs_entails_unseal=> ? HΔ.
+  rewrite envs_entails_unseal=> ? HΔ.
   rewrite -twp_bind. eapply wand_apply; first exact: twp_allocN.
   rewrite left_id. apply forall_intro=> l.
   specialize (HΔ l).
@@ -261,7 +261,7 @@ Lemma tac_wp_alloc Δ Δ' s E j K v Φ :
     end) →
   envs_entails Δ (WP fill K (Alloc (Val v)) @ s; E {{ Φ }}).
 Proof.
-  rewrite environments.envs_entails_unseal=> ? HΔ.
+  rewrite envs_entails_unseal=> ? HΔ.
   rewrite -wp_bind. eapply wand_apply; first exact: wp_alloc.
   rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
   specialize (HΔ l).
@@ -278,7 +278,7 @@ Lemma tac_twp_alloc Δ s E j K v Φ :
     end) →
   envs_entails Δ (WP fill K (Alloc (Val v)) @ s; E [{ Φ }]).
 Proof.
-  rewrite environments.envs_entails_unseal=> HΔ.
+  rewrite envs_entails_unseal=> HΔ.
   rewrite -twp_bind. eapply wand_apply; first exact: twp_alloc.
   rewrite left_id. apply forall_intro=> l.
   specialize (HΔ l).
@@ -294,7 +294,7 @@ Lemma tac_wp_free Δ Δ' s E i K l v Φ :
    envs_entails Δ'' (WP fill K (Val $ LitV LitUnit) @ s; E {{ Φ }})) →
   envs_entails Δ (WP fill K (Free (LitV l)) @ s; E {{ Φ }}).
 Proof.
-  rewrite environments.envs_entails_unseal=> ? Hlk Hfin.
+  rewrite envs_entails_unseal=> ? Hlk Hfin.
   rewrite -wp_bind. eapply wand_apply; first exact: wp_free.
   rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
   rewrite -Hfin wand_elim_r (envs_lookup_sound' _ _ _ _ _ Hlk).
@@ -306,7 +306,7 @@ Lemma tac_twp_free Δ s E i K l v Φ :
    envs_entails Δ' (WP fill K (Val $ LitV LitUnit) @ s; E [{ Φ }])) →
   envs_entails Δ (WP fill K (Free (LitV l)) @ s; E [{ Φ }]).
 Proof.
-  rewrite environments.envs_entails_unseal=> Hlk Hfin.
+  rewrite envs_entails_unseal=> Hlk Hfin.
   rewrite -twp_bind. eapply wand_apply; first exact: twp_free.
   rewrite envs_lookup_split //; simpl.
   rewrite -Hfin wand_elim_r (envs_lookup_sound' _ _ _ _ _ Hlk).
@@ -319,7 +319,7 @@ Lemma tac_wp_load Δ Δ' s E i K b l q v Φ :
   envs_entails Δ' (WP fill K (Val v) @ s; E {{ Φ }}) →
   envs_entails Δ (WP fill K (Load (LitV l)) @ s; E {{ Φ }}).
 Proof.
-  rewrite environments.envs_entails_unseal=> ?? Hi.
+  rewrite envs_entails_unseal=> ?? Hi.
   rewrite -wp_bind. eapply wand_apply; first exact: wp_load.
   rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
   apply later_mono.
@@ -332,7 +332,7 @@ Lemma tac_twp_load Δ s E i K b l q v Φ :
   envs_entails Δ (WP fill K (Val v) @ s; E [{ Φ }]) →
   envs_entails Δ (WP fill K (Load (LitV l)) @ s; E [{ Φ }]).
 Proof.
-  rewrite environments.envs_entails_unseal=> ? Hi.
+  rewrite envs_entails_unseal=> ? Hi.
   rewrite -twp_bind. eapply wand_apply; first exact: twp_load.
   rewrite envs_lookup_split //; simpl.
   destruct b; simpl.
@@ -349,7 +349,7 @@ Lemma tac_wp_store Δ Δ' s E i K l v v' Φ :
   end →
   envs_entails Δ (WP fill K (Store (LitV l) (Val v')) @ s; E {{ Φ }}).
 Proof.
-  rewrite environments.envs_entails_unseal=> ???.
+  rewrite envs_entails_unseal=> ???.
   destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
   rewrite -wp_bind. eapply wand_apply; first by eapply wp_store.
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
@@ -363,7 +363,7 @@ Lemma tac_twp_store Δ s E i K l v v' Φ :
   end →
   envs_entails Δ (WP fill K (Store (LitV l) v') @ s; E [{ Φ }]).
 Proof.
-  rewrite environments.envs_entails_unseal. intros.
+  rewrite envs_entails_unseal. intros.
   destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
   rewrite -twp_bind. eapply wand_apply; first by eapply twp_store.
   rewrite envs_simple_replace_sound //; simpl.
@@ -379,7 +379,7 @@ Lemma tac_wp_xchg Δ Δ' s E i K l v v' Φ :
   end →
   envs_entails Δ (WP fill K (Xchg (LitV l) (Val v')) @ s; E {{ Φ }}).
 Proof.
-  rewrite environments.envs_entails_unseal=> ???.
+  rewrite envs_entails_unseal=> ???.
   destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
   rewrite -wp_bind. eapply wand_apply; first by eapply wp_xchg.
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
@@ -394,7 +394,7 @@ Lemma tac_twp_xchg Δ s E i K l v v' Φ :
   end →
   envs_entails Δ (WP fill K (Xchg (LitV l) v') @ s; E [{ Φ }]).
 Proof.
-  rewrite environments.envs_entails_unseal. intros.
+  rewrite envs_entails_unseal. intros.
   destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
   rewrite -twp_bind. eapply wand_apply; first by eapply twp_xchg.
   rewrite envs_simple_replace_sound //; simpl.
@@ -415,7 +415,7 @@ Lemma tac_wp_cmpxchg Δ Δ' s E i K l v v1 v2 Φ :
    envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E {{ Φ }})) →
   envs_entails Δ (WP fill K (CmpXchg (LitV l) (Val v1) (Val v2)) @ s; E {{ Φ }}).
 Proof.
-  rewrite environments.envs_entails_unseal=> ??? Hsuc Hfail.
+  rewrite envs_entails_unseal=> ??? Hsuc Hfail.
   destruct (envs_simple_replace _ _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
   destruct (decide (v = v1)) as [Heq|Hne].
   - rewrite -wp_bind. eapply wand_apply.
@@ -440,7 +440,7 @@ Lemma tac_twp_cmpxchg Δ s E i K l v v1 v2 Φ :
    envs_entails Δ (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E [{ Φ }])) →
   envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E [{ Φ }]).
 Proof.
-  rewrite environments.envs_entails_unseal=> ?? Hsuc Hfail.
+  rewrite envs_entails_unseal=> ?? Hsuc Hfail.
   destruct (envs_simple_replace _ _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
   destruct (decide (v = v1)) as [Heq|Hne].
   - rewrite -twp_bind. eapply wand_apply.
@@ -460,7 +460,7 @@ Lemma tac_wp_cmpxchg_fail Δ Δ' s E i K l q v v1 v2 Φ :
   envs_entails Δ' (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E {{ Φ }}) →
   envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E {{ Φ }}).
 Proof.
-  rewrite environments.envs_entails_unseal=> ?????.
+  rewrite envs_entails_unseal=> ?????.
   rewrite -wp_bind. eapply wand_apply; first exact: wp_cmpxchg_fail.
   rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
@@ -471,7 +471,7 @@ Lemma tac_twp_cmpxchg_fail Δ s E i K l q v v1 v2 Φ :
   envs_entails Δ (WP fill K (Val $ PairV v (LitV $ LitBool false)) @ s; E [{ Φ }]) →
   envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E [{ Φ }]).
 Proof.
-  rewrite environments.envs_entails_unseal. intros. rewrite -twp_bind.
+  rewrite envs_entails_unseal. intros. rewrite -twp_bind.
   eapply wand_apply; first exact: twp_cmpxchg_fail.
   (* [//] solves some evars and enables further simplification. *)
   rewrite envs_lookup_split /= // /=. by do 2 f_equiv.
@@ -488,7 +488,7 @@ Lemma tac_wp_cmpxchg_suc Δ Δ' s E i K l v v1 v2 Φ :
   end →
   envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E {{ Φ }}).
 Proof.
-  rewrite environments.envs_entails_unseal=> ?????; subst.
+  rewrite envs_entails_unseal=> ?????; subst.
   destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
   rewrite -wp_bind. eapply wand_apply.
   { eapply wp_cmpxchg_suc; eauto. }
@@ -505,7 +505,7 @@ Lemma tac_twp_cmpxchg_suc Δ s E i K l v v1 v2 Φ :
   end →
   envs_entails Δ (WP fill K (CmpXchg (LitV l) v1 v2) @ s; E [{ Φ }]).
 Proof.
-  rewrite environments.envs_entails_unseal=>????; subst.
+  rewrite envs_entails_unseal=>????; subst.
   destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
   rewrite -twp_bind. eapply wand_apply.
   { eapply twp_cmpxchg_suc; eauto. }
@@ -522,7 +522,7 @@ Lemma tac_wp_faa Δ Δ' s E i K l z1 z2 Φ :
   end →
   envs_entails Δ (WP fill K (FAA (LitV l) (LitV z2)) @ s; E {{ Φ }}).
 Proof.
-  rewrite environments.envs_entails_unseal=> ???.
+  rewrite envs_entails_unseal=> ???.
   destruct (envs_simple_replace _ _ _) as [Δ''|] eqn:HΔ''; [ | contradiction ].
   rewrite -wp_bind. eapply wand_apply; first exact: (wp_faa _ _ _ z1 z2).
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
@@ -536,7 +536,7 @@ Lemma tac_twp_faa Δ s E i K l z1 z2 Φ :
   end →
   envs_entails Δ (WP fill K (FAA (LitV l) (LitV z2)) @ s; E [{ Φ }]).
 Proof.
-  rewrite environments.envs_entails_unseal=> ??.
+  rewrite envs_entails_unseal=> ??.
   destruct (envs_simple_replace _ _ _) as [Δ'|] eqn:HΔ'; [ | contradiction ].
   rewrite -twp_bind. eapply wand_apply; first exact: (twp_faa _ _ _ z1 z2).
   rewrite envs_simple_replace_sound //; simpl.
diff --git a/tests/heapprop.v b/tests/heapprop.v
index 0efc4745a..31b5edbee 100644
--- a/tests/heapprop.v
+++ b/tests/heapprop.v
@@ -105,7 +105,7 @@ Local Definition heapProp_persistently_unseal:
 step-indexed logics, it can be defined as the identity. *)
 Definition heapProp_later (P : heapProp) : heapProp := P.
 
-Definition heapProp_unseal :=
+Local Definition heapProp_unseal :=
   (heapProp_emp_unseal, heapProp_pure_unseal, heapProp_and_unseal,
    heapProp_or_unseal, heapProp_impl_unseal, heapProp_forall_unseal,
    heapProp_exist_unseal, heapProp_sep_unseal, heapProp_wand_unseal,
-- 
GitLab