From 8574d1eab3892ce04870849e9445e406975a7f09 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 29 Oct 2017 01:29:03 +0200
Subject: [PATCH] Hide the proof mode entailment behind a definition.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This solves issue #100: the proof mode notation is sometimes not printed. As
Ralf discovered, the problem is that there are two overlapping notations:

```coq
Notation "P ⊢ Q" := (uPred_entails P Q).
```

And the "proof mode" notation:

```
Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q" :=
  (of_envs (Envs Γ Δ) ⊢ Q%I).
```

These two notations overlap, so, when having a "proof mode" goal of the shape
`of_envs (Envs Γ Δ) ⊢ Q%I`, how do we know which notation is Coq going to pick
for pretty printing this goal? As we have seen, this choice depends on the
import order (since both notations appear in different files), and as such, Coq
sometimes (unintendedly) uses the first notation instead of the latter.

The idea of this commit is to wrap `of_envs (Envs Γ Δ) ⊢ Q%I` into a definition
so that there is no ambiguity for the pretty printer anymore.
---
 theories/base_logic/base_logic.v        |   2 +-
 theories/base_logic/big_op.v            |   7 +-
 theories/base_logic/lib/fancy_updates.v |   2 +-
 theories/heap_lang/proofmode.v          |  71 +++--
 theories/proofmode/coq_tactics.v        | 334 ++++++++++++++----------
 theories/proofmode/notation.v           |   9 +-
 theories/proofmode/tactics.v            |  96 +++----
 theories/tests/proofmode.v              |   2 +-
 8 files changed, 301 insertions(+), 222 deletions(-)

diff --git a/theories/base_logic/base_logic.v b/theories/base_logic/base_logic.v
index 58a5a0098..05ac2922c 100644
--- a/theories/base_logic/base_logic.v
+++ b/theories/base_logic/base_logic.v
@@ -8,7 +8,7 @@ Module Import uPred.
 End uPred.
 
 (* Hint DB for the logic *)
-Hint Resolve pure_intro.
+Hint Resolve pure_intro : I.
 Hint Resolve or_elim or_intro_l' or_intro_r' : I.
 Hint Resolve and_intro and_elim_l' and_elim_r' : I.
 Hint Resolve persistently_mono : I.
diff --git a/theories/base_logic/big_op.v b/theories/base_logic/big_op.v
index 3d6f774a5..3ff02f9d0 100644
--- a/theories/base_logic/big_op.v
+++ b/theories/base_logic/big_op.v
@@ -330,7 +330,7 @@ Section gmap.
     intros. apply (anti_symm _).
     { apply forall_intro=> k; apply forall_intro=> x.
       apply impl_intro_l, pure_elim_l=> ?; by apply big_sepM_lookup. }
-    induction m as [|i x m ? IH] using map_ind; [rewrite ?big_sepM_empty; auto|].
+    induction m as [|i x m ? IH] using map_ind; auto using big_sepM_empty'.
     rewrite big_sepM_insert // -and_sep_l. apply and_intro.
     - rewrite (forall_elim i) (forall_elim x) lookup_insert.
       by rewrite pure_True // True_impl.
@@ -488,8 +488,7 @@ Section gset.
     intros. apply (anti_symm _).
     { apply forall_intro=> x.
       apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. }
-    induction X as [|x X ? IH] using collection_ind_L.
-    { rewrite big_sepS_empty; auto. }
+    induction X as [|x X ? IH] using collection_ind_L; auto using big_sepS_empty'.
     rewrite big_sepS_insert // -and_sep_l. apply and_intro.
     - by rewrite (forall_elim x) pure_True ?True_impl; last set_solver.
     - rewrite -IH. apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
@@ -619,5 +618,3 @@ Section gmultiset.
   Proof. rewrite /big_opMS. apply _. Qed.
 End gmultiset.
 End big_op.
-
-Hint Resolve big_sepL_nil' big_sepM_empty' big_sepS_empty' big_sepMS_empty' | 0.
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index e8e55cf13..5b5cd98d8 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -224,7 +224,7 @@ Section proofmode_classes.
   Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_trans. Qed.
 End proofmode_classes.
 
-Hint Extern 2 (coq_tactics.of_envs _ ⊢ |={_}=> _) => iModIntro.
+Hint Extern 2 (coq_tactics.envs_entails _ (|={_}=> _)) => iModIntro.
 
 (** Fancy updates that take a step. *)
 
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 503b21286..8a047e571 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -9,20 +9,25 @@ Lemma tac_wp_pure `{heapG Σ} K Δ Δ' E e1 e2 φ Φ :
   PureExec φ e1 e2 →
   φ →
   IntoLaterNEnvs 1 Δ Δ' →
-  (Δ' ⊢ WP fill K e2 @ E {{ Φ }}) →
-  (Δ ⊢ WP fill K e1 @ E {{ Φ }}).
+  envs_entails Δ' (WP fill K e2 @ E {{ Φ }}) →
+  envs_entails Δ (WP fill K e1 @ E {{ Φ }}).
 Proof.
-  intros ??? HΔ'. rewrite into_laterN_env_sound /=.
+  rewrite /envs_entails=> ??? HΔ'. rewrite into_laterN_env_sound /=.
   rewrite -lifting.wp_bind HΔ' -wp_pure_step_later //.
   by rewrite -ectx_lifting.wp_ectx_bind_inv.
 Qed.
 
-Ltac wp_value_head := etrans; [|eapply wp_value; apply _]; simpl.
+Lemma tac_wp_value `{heapG Σ} Δ E Φ e v :
+  IntoVal e v →
+  envs_entails Δ (Φ v) → envs_entails Δ (WP e @ E {{ Φ }}).
+Proof. rewrite /envs_entails=> ? ->. by apply wp_value. Qed.
+
+Ltac wp_value_head := eapply tac_wp_value; [apply _|lazy beta].
 
 Tactic Notation "wp_pure" open_constr(efoc) :=
   iStartProof;
   lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+  | |- envs_entails _ (wp ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
     unify e' efoc;
     eapply (tac_wp_pure K);
     [simpl; apply _                 (* PureExec *)
@@ -47,16 +52,21 @@ 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.
 
+Lemma tac_wp_bind `{heapG Σ} K Δ E Φ e :
+  envs_entails Δ (WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }})%I →
+  envs_entails Δ (WP fill K e @ E {{ Φ }}).
+Proof. rewrite /envs_entails=> ->. by apply wp_bind. Qed.
+
 Ltac wp_bind_core K :=
   lazymatch eval hnf in K with
   | [] => idtac
-  | _ => etrans; [|fast_by apply (wp_bind K)]; simpl
+  | _ => apply (tac_wp_bind K); simpl
   end.
 
 Tactic Notation "wp_bind" open_constr(efoc) :=
   iStartProof;
   lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
+  | |- envs_entails _ (wp ?E ?e ?Q) => reshape_expr e ltac:(fun K e' =>
     match e' with
     | efoc => unify e' efoc; wp_bind_core K
     end) || fail "wp_bind: cannot find" efoc "in" e
@@ -75,10 +85,11 @@ Lemma tac_wp_alloc Δ Δ' E j K e v Φ :
   IntoLaterNEnvs 1 Δ Δ' →
   (∀ l, ∃ Δ'',
     envs_app false (Esnoc Enil j (l ↦ v)) Δ' = Some Δ'' ∧
-    (Δ'' ⊢ WP fill K (Lit (LitLoc l)) @ E {{ Φ }})) →
-  Δ ⊢ WP fill K (Alloc e) @ E {{ Φ }}.
+    envs_entails Δ'' (WP fill K (Lit (LitLoc l)) @ E {{ Φ }})) →
+  envs_entails Δ (WP fill K (Alloc e) @ E {{ Φ }}).
 Proof.
-  intros ?? HΔ. rewrite -wp_bind. eapply wand_apply; first exact: wp_alloc.
+  rewrite /envs_entails=> ?? HΔ.
+  rewrite -wp_bind. eapply wand_apply; first exact: wp_alloc.
   rewrite left_id into_laterN_env_sound; apply later_mono, forall_intro=> l.
   destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
   by rewrite right_id HΔ'.
@@ -87,10 +98,11 @@ Qed.
 Lemma tac_wp_load Δ Δ' E i K l q v Φ :
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I →
-  (Δ' ⊢ WP fill K (of_val v) @ E {{ Φ }}) →
-  Δ ⊢ WP fill K (Load (Lit (LitLoc l))) @ E {{ Φ }}.
+  envs_entails Δ' (WP fill K (of_val v) @ E {{ Φ }}) →
+  envs_entails Δ (WP fill K (Load (Lit (LitLoc l))) @ E {{ Φ }}).
 Proof.
-  intros. rewrite -wp_bind. eapply wand_apply; first exact: wp_load.
+  rewrite /envs_entails=> ???.
+  rewrite -wp_bind. eapply wand_apply; first exact: wp_load.
   rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
@@ -100,10 +112,11 @@ Lemma tac_wp_store Δ Δ' Δ'' E i K l v e v' Φ :
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
-  (Δ'' ⊢ WP fill K (Lit LitUnit) @ E {{ Φ }}) →
-  Δ ⊢ WP fill K (Store (Lit (LitLoc l)) e) @ E {{ Φ }}.
+  envs_entails Δ'' (WP fill K (Lit LitUnit) @ E {{ Φ }}) →
+  envs_entails Δ (WP fill K (Store (Lit (LitLoc l)) e) @ E {{ Φ }}).
 Proof.
-  intros. rewrite -wp_bind. eapply wand_apply; first by eapply wp_store.
+  rewrite /envs_entails=> ?????.
+  rewrite -wp_bind. eapply wand_apply; first by eapply wp_store.
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
@@ -112,10 +125,11 @@ Lemma tac_wp_cas_fail Δ Δ' E i K l q v e1 v1 e2 Φ :
   IntoVal e1 v1 → AsVal e2 →
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦{q} v)%I → v ≠ v1 →
-  (Δ' ⊢ WP fill K (Lit (LitBool false)) @ E {{ Φ }}) →
-  Δ ⊢ WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ E {{ Φ }}.
+  envs_entails Δ' (WP fill K (Lit (LitBool false)) @ E {{ Φ }}) →
+  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ E {{ Φ }}).
 Proof.
-  intros. rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_fail.
+  rewrite /envs_entails=> ??????.
+  rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_fail.
   rewrite into_laterN_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
@@ -125,10 +139,11 @@ Lemma tac_wp_cas_suc Δ Δ' Δ'' E i K l v e1 v1 e2 v2 Φ :
   IntoLaterNEnvs 1 Δ Δ' →
   envs_lookup i Δ' = Some (false, l ↦ v)%I → v = v1 →
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
-  (Δ'' ⊢ WP fill K (Lit (LitBool true)) @ E {{ Φ }}) →
-  Δ ⊢ WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ E {{ Φ }}.
+  envs_entails Δ'' (WP fill K (Lit (LitBool true)) @ E {{ Φ }}) →
+  envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ E {{ Φ }}).
 Proof.
-  intros; subst. rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_suc.
+  rewrite /envs_entails=> ???????; subst.
+  rewrite -wp_bind. eapply wand_apply; first exact: wp_cas_suc.
   rewrite into_laterN_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
@@ -137,7 +152,7 @@ End heap.
 Tactic Notation "wp_apply" open_constr(lem) :=
   iPoseProofCore lem as false true (fun H =>
     lazymatch goal with
-    | |- _ ⊢ wp ?E ?e ?Q =>
+    | |- envs_entails _ (wp ?E ?e ?Q) =>
       reshape_expr e ltac:(fun K e' =>
         wp_bind_core K; iApplyHyp H; try iNext; simpl) ||
       lazymatch iTypeOf H with
@@ -149,7 +164,7 @@ Tactic Notation "wp_apply" open_constr(lem) :=
 Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
   iStartProof;
   lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q =>
+  | |- envs_entails _ (wp ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
          eapply (tac_wp_alloc _ _ _ H K); [apply _|..])
@@ -168,7 +183,7 @@ Tactic Notation "wp_alloc" ident(l) :=
 Tactic Notation "wp_load" :=
   iStartProof;
   lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q =>
+  | |- envs_entails _ (wp ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' => eapply (tac_wp_load _ _ _ _ K))
       |fail 1 "wp_load: cannot find 'Load' in" e];
@@ -182,7 +197,7 @@ Tactic Notation "wp_load" :=
 Tactic Notation "wp_store" :=
   iStartProof;
   lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q =>
+  | |- envs_entails _ (wp ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
          eapply (tac_wp_store _ _ _ _ _ K); [apply _|..])
@@ -198,7 +213,7 @@ Tactic Notation "wp_store" :=
 Tactic Notation "wp_cas_fail" :=
   iStartProof;
   lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q =>
+  | |- envs_entails _ (wp ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
          eapply (tac_wp_cas_fail _ _ _ _ K); [apply _|apply _|..])
@@ -214,7 +229,7 @@ Tactic Notation "wp_cas_fail" :=
 Tactic Notation "wp_cas_suc" :=
   iStartProof;
   lazymatch goal with
-  | |- _ ⊢ wp ?E ?e ?Q =>
+  | |- envs_entails _ (wp ?E ?e ?Q) =>
     first
       [reshape_expr e ltac:(fun K e' =>
          eapply (tac_wp_cas_suc _ _ _ _ _ K); [apply _|apply _|..])
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 9ef1ff584..5867734c7 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -21,10 +21,16 @@ Record envs_wf {M} (Δ : envs M) := {
   envs_disjoint i : env_persistent Δ !! i = None ∨ env_spatial Δ !! i = None
 }.
 
-Coercion of_envs {M} (Δ : envs M) : uPred M :=
+Definition of_envs {M} (Δ : envs M) : uPred M :=
   (⌜envs_wf Δ⌝ ∗ □ [∗] env_persistent Δ ∗ [∗] env_spatial Δ)%I.
 Instance: Params (@of_envs) 1.
 
+Definition envs_entails {M} (Δ : envs M) (Q : uPred M) : Prop :=
+  of_envs Δ ⊢ Q.
+Arguments envs_entails {_} _ _%I.
+Typeclasses Opaque envs_entails.
+Instance: Params (@envs_entails) 1.
+
 Record envs_Forall2 {M} (R : relation (uPred M)) (Δ1 Δ2 : envs M) : Prop := {
   env_persistent_Forall2 : env_Forall2 R (env_persistent Δ1) (env_persistent Δ2);
   env_spatial_Forall2 : env_Forall2 R (env_spatial Δ1) (env_spatial Δ2)
@@ -136,7 +142,8 @@ Proof.
 Qed.
 
 Lemma envs_lookup_sound Δ i p P :
-  envs_lookup i Δ = Some (p,P) → Δ ⊢ □?p P ∗ envs_delete i p Δ.
+  envs_lookup i Δ = Some (p,P) →
+  of_envs Δ ⊢ □?p P ∗ of_envs (envs_delete i p Δ).
 Proof.
   rewrite /envs_lookup /envs_delete /of_envs=>?; apply pure_elim_sep_l=> Hwf.
   destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
@@ -151,16 +158,17 @@ Proof.
       naive_solver eauto using env_delete_wf, env_delete_fresh.
 Qed.
 Lemma envs_lookup_sound' Δ i p P :
-  envs_lookup i Δ = Some (p,P) → Δ ⊢ P ∗ envs_delete i p Δ.
+  envs_lookup i Δ = Some (p,P) →
+  of_envs Δ ⊢ P ∗ of_envs (envs_delete i p Δ).
 Proof. intros. rewrite envs_lookup_sound //. by rewrite persistently_if_elim. Qed.
 Lemma envs_lookup_persistent_sound Δ i P :
-  envs_lookup i Δ = Some (true,P) → Δ ⊢ □ P ∗ Δ.
+  envs_lookup i Δ = Some (true,P) → of_envs Δ ⊢ □ P ∗ of_envs Δ.
 Proof.
   intros. apply (persistently_entails_l _ _). by rewrite envs_lookup_sound // sep_elim_l.
 Qed.
 
 Lemma envs_lookup_split Δ i p P :
-  envs_lookup i Δ = Some (p,P) → Δ ⊢ □?p P ∗ (□?p P -∗ Δ).
+  envs_lookup i Δ = Some (p,P) → of_envs Δ ⊢ □?p P ∗ (□?p P -∗ of_envs Δ).
 Proof.
   rewrite /envs_lookup /of_envs=>?; apply pure_elim_sep_l=> Hwf.
   destruct Δ as [Γp Γs], (Γp !! i) eqn:?; simplify_eq/=.
@@ -173,14 +181,15 @@ Proof.
 Qed.
 
 Lemma envs_lookup_delete_sound Δ Δ' i p P :
-  envs_lookup_delete i Δ = Some (p,P,Δ') → Δ ⊢ □?p P ∗ Δ'.
+  envs_lookup_delete i Δ = Some (p,P,Δ') → of_envs Δ ⊢ □?p P ∗ of_envs Δ'.
 Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound. Qed.
 Lemma envs_lookup_delete_sound' Δ Δ' i p P :
-  envs_lookup_delete i Δ = Some (p,P,Δ') → Δ ⊢ P ∗ Δ'.
+  envs_lookup_delete i Δ = Some (p,P,Δ') → of_envs Δ ⊢ P ∗ of_envs Δ'.
 Proof. intros [? ->]%envs_lookup_delete_Some. by apply envs_lookup_sound'. Qed.
 
 Lemma envs_lookup_delete_list_sound Δ Δ' js rp p Ps :
-  envs_lookup_delete_list js rp Δ = Some (p, Ps,Δ') → Δ ⊢ □?p [∗] Ps ∗ Δ'.
+  envs_lookup_delete_list js rp Δ = Some (p, Ps,Δ') →
+  of_envs Δ ⊢ □?p [∗] Ps ∗ of_envs Δ'.
 Proof.
   revert Δ Δ' p Ps. induction js as [|j js IH]=> Δ Δ'' p Ps ?; simplify_eq/=.
   { by rewrite persistently_pure left_id. }
@@ -208,7 +217,7 @@ Proof.
 Qed.
 
 Lemma envs_snoc_sound Δ p i P :
-  envs_lookup i Δ = None → Δ ⊢ □?p P -∗ envs_snoc Δ p i P.
+  envs_lookup i Δ = None → of_envs Δ ⊢ □?p P -∗ of_envs (envs_snoc Δ p i P).
 Proof.
   rewrite /envs_lookup /envs_snoc /of_envs=> ?; apply pure_elim_sep_l=> Hwf.
   destruct Δ as [Γp Γs], (Γp !! i) eqn:?, (Γs !! i) eqn:?; simplify_eq/=.
@@ -223,7 +232,8 @@ Proof.
     + solve_sep_entails.
 Qed.
 
-Lemma envs_app_sound Δ Δ' p Γ : envs_app p Γ Δ = Some Δ' → Δ ⊢ □?p [∗] Γ -∗ Δ'.
+Lemma envs_app_sound Δ Δ' p Γ :
+  envs_app p Γ Δ = Some Δ' → of_envs Δ ⊢ □?p [∗] Γ -∗ of_envs Δ'.
 Proof.
   rewrite /of_envs /envs_app=> ?; apply pure_elim_sep_l=> Hwf.
   destruct Δ as [Γp Γs], p; simplify_eq/=.
@@ -246,7 +256,7 @@ Qed.
 
 Lemma envs_simple_replace_sound' Δ Δ' i p Γ :
   envs_simple_replace i p Γ Δ = Some Δ' →
-  envs_delete i p Δ ⊢ □?p [∗] Γ -∗ Δ'.
+  of_envs (envs_delete i p Δ) ⊢ □?p [∗] Γ -∗ of_envs Δ'.
 Proof.
   rewrite /envs_simple_replace /envs_delete /of_envs=> ?.
   apply pure_elim_sep_l=> Hwf. destruct Δ as [Γp Γs], p; simplify_eq/=.
@@ -269,11 +279,12 @@ Qed.
 
 Lemma envs_simple_replace_sound Δ Δ' i p P Γ :
   envs_lookup i Δ = Some (p,P) → envs_simple_replace i p Γ Δ = Some Δ' →
-  Δ ⊢ □?p P ∗ (□?p [∗] Γ -∗ Δ').
+  of_envs Δ ⊢ □?p P ∗ (□?p [∗] Γ -∗ of_envs Δ').
 Proof. intros. by rewrite envs_lookup_sound// envs_simple_replace_sound'//. Qed.
 
 Lemma envs_replace_sound' Δ Δ' i p q Γ :
-  envs_replace i p q Γ Δ = Some Δ' → envs_delete i p Δ ⊢ □?q [∗] Γ -∗ Δ'.
+  envs_replace i p q Γ Δ = Some Δ' →
+  of_envs (envs_delete i p Δ) ⊢ □?q [∗] Γ -∗ of_envs Δ'.
 Proof.
   rewrite /envs_replace; destruct (eqb _ _) eqn:Hpq.
   - apply eqb_prop in Hpq as ->. apply envs_simple_replace_sound'.
@@ -282,7 +293,7 @@ Qed.
 
 Lemma envs_replace_sound Δ Δ' i p q P Γ :
   envs_lookup i Δ = Some (p,P) → envs_replace i p q Γ Δ = Some Δ' →
-  Δ ⊢ □?p P ∗ (□?q [∗] Γ -∗ Δ').
+  of_envs Δ ⊢ □?p P ∗ (□?q [∗] Γ -∗ of_envs Δ').
 Proof. intros. by rewrite envs_lookup_sound// envs_replace_sound'//. Qed.
 
 Lemma envs_lookup_envs_clear_spatial Δ j :
@@ -294,7 +305,8 @@ Proof.
   by destruct (Γs !! j).
 Qed.
 
-Lemma envs_clear_spatial_sound Δ : Δ ⊢ envs_clear_spatial Δ ∗ [∗] env_spatial Δ.
+Lemma envs_clear_spatial_sound Δ :
+  of_envs Δ ⊢ of_envs (envs_clear_spatial Δ) ∗ [∗] env_spatial Δ.
 Proof.
   rewrite /of_envs /envs_clear_spatial /=; apply pure_elim_sep_l=> Hwf.
   rewrite right_id -assoc; apply sep_intro_True_l; [apply pure_intro|done].
@@ -302,7 +314,7 @@ Proof.
 Qed.
 
 Lemma env_spatial_is_nil_persistent Δ :
-  env_spatial_is_nil Δ = true → Persistent Δ.
+  env_spatial_is_nil Δ = true → Persistent (of_envs Δ).
 Proof. intros; destruct Δ as [? []]; simplify_eq/=; apply _. Qed.
 Hint Immediate env_spatial_is_nil_persistent : typeclass_instances.
 
@@ -326,7 +338,8 @@ Qed.
 
 Lemma envs_split_go_sound js Δ1 Δ2 Δ1' Δ2' :
   (∀ j P, envs_lookup j Δ1 = Some (false, P) → envs_lookup j Δ2 = None) →
-  envs_split_go js Δ1 Δ2 = Some (Δ1',Δ2') → Δ1 ∗ Δ2 ⊢ Δ1' ∗ Δ2'.
+  envs_split_go js Δ1 Δ2 = Some (Δ1',Δ2') →
+  of_envs Δ1 ∗ of_envs Δ2 ⊢ of_envs Δ1' ∗ of_envs Δ2'.
 Proof.
   revert Δ1 Δ2 Δ1' Δ2'.
   induction js as [|j js IH]=> Δ1 Δ2 Δ1' Δ2' Hlookup HΔ; simplify_eq/=; [done|].
@@ -342,9 +355,9 @@ Proof.
   rewrite (envs_snoc_sound Δ2 false j P) /= ?wand_elim_r; eauto.
 Qed.
 Lemma envs_split_sound Δ d js Δ1 Δ2 :
-  envs_split d js Δ = Some (Δ1,Δ2) → Δ ⊢ Δ1 ∗ Δ2.
+  envs_split d js Δ = Some (Δ1,Δ2) → of_envs Δ ⊢ of_envs Δ1 ∗ of_envs Δ2.
 Proof.
-  rewrite /envs_split=> ?. rewrite -(idemp uPred_and Δ).
+  rewrite /envs_split=> ?. rewrite -(idemp uPred_and (of_envs Δ)).
   rewrite {2}envs_clear_spatial_sound sep_elim_l and_sep_r.
   destruct (envs_split_go _ _) as [[Δ1' Δ2']|] eqn:HΔ; [|done].
   apply envs_split_go_sound in HΔ as ->; last first.
@@ -381,52 +394,65 @@ Proof.
   intros Δ1 Δ2 HΔ; apply (anti_symm (⊢)); apply of_envs_mono;
     eapply (envs_Forall2_impl (⊣⊢)); [| |symmetry|]; eauto using equiv_entails.
 Qed.
-Global Instance Envs_mono (R : relation (uPred M)) :
+
+Global Instance Envs_proper (R : relation (uPred M)) :
   Proper (env_Forall2 R ==> env_Forall2 R ==> envs_Forall2 R) (@Envs M).
 Proof. by constructor. Qed.
 
+Global Instance envs_entails_proper :
+  Proper (envs_Forall2 (⊣⊢) ==> (⊣⊢) ==> iff) (@envs_entails M).
+Proof. solve_proper. Qed.
+Global Instance envs_entails_flip_mono :
+  Proper (envs_Forall2 (⊢) ==> flip (⊢) ==> flip impl) (@envs_entails M).
+Proof. rewrite /envs_entails=> Δ1 Δ2 ? P1 P2 <- <-. by f_equiv. Qed.
+
 (** * Adequacy *)
-Lemma tac_adequate P : (Envs Enil Enil ⊢ P) → P.
+Lemma tac_adequate P : envs_entails (Envs Enil Enil) P → P.
 Proof.
-  intros <-. rewrite /of_envs /= persistently_pure !right_id.
+  rewrite /envs_entails=> <-. rewrite /of_envs /= persistently_pure !right_id.
   apply pure_intro; repeat constructor.
 Qed.
 
 (** * Basic rules *)
 Lemma tac_assumption Δ i p P Q :
-  envs_lookup i Δ = Some (p,P) → FromAssumption p P Q → Δ ⊢ Q.
-Proof. intros. by rewrite envs_lookup_sound // sep_elim_l. Qed.
+  envs_lookup i Δ = Some (p,P) → FromAssumption p P Q →
+  envs_entails Δ Q.
+Proof. intros. by rewrite /envs_entails envs_lookup_sound // sep_elim_l. Qed.
 
 Lemma tac_rename Δ Δ' i j p P Q :
   envs_lookup i Δ = Some (p,P) →
   envs_simple_replace i p (Esnoc Enil j P) Δ = Some Δ' →
-  (Δ' ⊢ Q) → Δ ⊢ Q.
+  envs_entails Δ' Q →
+  envs_entails Δ Q.
 Proof.
-  intros. rewrite envs_simple_replace_sound //.
+  rewrite /envs_entails=> ?? <-. rewrite envs_simple_replace_sound //.
   destruct p; simpl; by rewrite right_id wand_elim_r.
 Qed.
 Lemma tac_clear Δ Δ' i p P Q :
-  envs_lookup_delete i Δ = Some (p,P,Δ') → (Δ' ⊢ Q) → Δ ⊢ Q.
-Proof. intros. by rewrite envs_lookup_delete_sound // sep_elim_r. Qed.
+  envs_lookup_delete i Δ = Some (p,P,Δ') →
+  envs_entails Δ' Q → envs_entails Δ Q.
+Proof.
+  rewrite /envs_entails=> ? <-. by rewrite envs_lookup_delete_sound // sep_elim_r.
+Qed.
 
 (** * False *)
-Lemma tac_ex_falso Δ Q : (Δ ⊢ False) → Δ ⊢ Q.
-Proof. by rewrite -(False_elim Q). Qed.
+Lemma tac_ex_falso Δ Q : envs_entails Δ False → envs_entails Δ Q.
+Proof. by rewrite /envs_entails -(False_elim Q). Qed.
 
 (** * Pure *)
-Lemma tac_pure_intro Δ Q (φ : Prop) : FromPure Q φ → φ → Δ ⊢ Q.
-Proof. intros ??. rewrite -(from_pure Q). by apply pure_intro. Qed.
+Lemma tac_pure_intro Δ Q φ : FromPure Q φ → φ → envs_entails Δ Q.
+Proof. intros ??. rewrite /envs_entails -(from_pure Q). by apply pure_intro. Qed.
 
 Lemma tac_pure Δ Δ' i p P φ Q :
   envs_lookup_delete i Δ = Some (p, P, Δ') → IntoPure P φ →
-  (φ → Δ' ⊢ Q) → Δ ⊢ Q.
+  (φ → envs_entails Δ' Q) → envs_entails Δ Q.
 Proof.
-  intros ?? HQ. rewrite envs_lookup_delete_sound' //; simpl.
+  rewrite /envs_entails=> ?? HQ. rewrite envs_lookup_delete_sound' //; simpl.
   rewrite (into_pure P); by apply pure_elim_sep_l.
 Qed.
 
-Lemma tac_pure_revert Δ φ Q : (Δ ⊢ ⌜φ⌝ → Q) → (φ → Δ ⊢ Q).
-Proof. intros HΔ ?. by rewrite HΔ pure_True // left_id. Qed.
+Lemma tac_pure_revert Δ φ Q : envs_entails Δ (⌜φ⌝ → Q) → (φ → envs_entails Δ Q).
+Proof. rewrite /envs_entails. intros HΔ ?. by rewrite HΔ pure_True // left_id. Qed.
 
 (** * Later *)
 Class IntoLaterNEnv (n : nat) (Γ1 Γ2 : env (uPred M)) :=
@@ -448,7 +474,8 @@ Global Instance into_laterN_envs n Γp1 Γp2 Γs1 Γs2 :
   IntoLaterNEnvs n (Envs Γp1 Γs1) (Envs Γp2 Γs2).
 Proof. by split. Qed.
 
-Lemma into_laterN_env_sound n Δ1 Δ2 : IntoLaterNEnvs n Δ1 Δ2 → Δ1 ⊢ ▷^n Δ2.
+Lemma into_laterN_env_sound n Δ1 Δ2 :
+  IntoLaterNEnvs n Δ1 Δ2 → of_envs Δ1 ⊢ ▷^n (of_envs Δ2).
 Proof.
   intros [Hp Hs]; rewrite /of_envs /= !laterN_sep -persistently_laterN.
   repeat apply sep_mono; try apply persistently_mono.
@@ -459,15 +486,20 @@ Proof.
 Qed.
 
 Lemma tac_next Δ Δ' n Q Q' :
-  FromLaterN n Q Q' → IntoLaterNEnvs n Δ Δ' → (Δ' ⊢ Q') → Δ ⊢ Q.
-Proof. intros ?? HQ. by rewrite -(from_laterN n Q) into_laterN_env_sound HQ. Qed.
+  FromLaterN n Q Q' → IntoLaterNEnvs n Δ Δ' →
+  envs_entails Δ' Q' → envs_entails Δ Q.
+Proof.
+  rewrite /envs_entails=> ?? HQ.
+  by rewrite -(from_laterN n Q) into_laterN_env_sound HQ.
+Qed.
 
 Lemma tac_löb Δ Δ' i Q :
   env_spatial_is_nil Δ = true →
   envs_app true (Esnoc Enil i (▷ Q)%I) Δ = Some Δ' →
-  (Δ' ⊢ Q) → Δ ⊢ Q.
+  envs_entails Δ' Q → envs_entails Δ Q.
 Proof.
-  intros ?? HQ. rewrite -(persistently_elim Q) -(löb (□ Q)) -persistently_later.
+  rewrite /envs_entails=> ?? HQ.
+  rewrite -(persistently_elim Q) -(löb (□ Q)) -persistently_later.
   apply impl_intro_l, (persistently_intro _ _).
   rewrite envs_app_sound //; simpl.
   by rewrite right_id persistently_and_sep_l wand_elim_r HQ.
@@ -504,7 +536,8 @@ Global Instance into_persistent_envs_true Γp1 Γp2 Γs1 :
 Proof. by split. Qed.
 
 Lemma into_persistent_envs_sound (p : bool) Δ1 Δ2 :
-  IntoPersistentEnvs p Δ1 Δ2 → Δ1 ⊢ (if p then ■ Δ2 else □ Δ2).
+  IntoPersistentEnvs p Δ1 Δ2 →
+  of_envs Δ1 ⊢ (if p then ■ of_envs Δ2 else □ of_envs Δ2).
 Proof.
   rewrite /of_envs. destruct Δ1 as [Γp1 Γs1], Δ2 as [Γp2 Γs2]=> -[/= Hp ->].
   apply pure_elim_sep_l=> Hwf. rewrite sep_elim_l. destruct p; simplify_eq/=.
@@ -521,9 +554,10 @@ Qed.
 Lemma tac_always_intro Δ Δ' p Q Q' :
   FromAlways p Q' Q →
   IntoPersistentEnvs p Δ Δ' →
-  (Δ' ⊢ Q) → Δ ⊢ Q'.
+  envs_entails Δ' Q → envs_entails Δ Q'.
 Proof.
-  intros ?? HQ. rewrite into_persistent_envs_sound -(from_always _ Q').
+  rewrite /envs_entails=> ?? HQ.
+  rewrite into_persistent_envs_sound -(from_always _ Q').
   destruct p; auto using persistently_mono, plainly_mono.
 Qed.
 
@@ -531,9 +565,9 @@ Lemma tac_persistent Δ Δ' i p P P' Q :
   envs_lookup i Δ = Some (p, P) →
   IntoPersistent p P P' →
   envs_replace i p true (Esnoc Enil i P') Δ = Some Δ' →
-  (Δ' ⊢ Q) → Δ ⊢ Q.
+  envs_entails Δ' Q → envs_entails Δ Q.
 Proof.
-  intros ? HP ? <-. rewrite envs_replace_sound //; simpl.
+  rewrite /envs_entails=> ? HP ? <-. rewrite envs_replace_sound //; simpl.
   by rewrite right_id (into_persistent _ P) wand_elim_r.
 Qed.
 
@@ -541,10 +575,10 @@ Qed.
 Lemma tac_impl_intro Δ Δ' i P Q :
   (if env_spatial_is_nil Δ then TCTrue else Persistent P) →
   envs_app false (Esnoc Enil i P) Δ = Some Δ' →
-  (Δ' ⊢ Q) → Δ ⊢ P → Q.
+  envs_entails Δ' Q → envs_entails Δ (P → Q).
 Proof.
-  intros ?? <-. destruct (env_spatial_is_nil Δ) eqn:?.
-  - rewrite (persistent Δ) envs_app_sound //; simpl.
+  rewrite /envs_entails=> ?? <-. destruct (env_spatial_is_nil Δ) eqn:?.
+  - rewrite (persistent (of_envs Δ)) envs_app_sound //; simpl.
     by rewrite right_id -persistently_impl_wand persistently_elim.
   - apply impl_intro_l. rewrite envs_app_sound //; simpl.
     by rewrite and_sep_l right_id wand_elim_r.
@@ -552,31 +586,34 @@ Qed.
 Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
   IntoPersistent false P P' →
   envs_app true (Esnoc Enil i P') Δ = Some Δ' →
-  (Δ' ⊢ Q) → Δ ⊢ P → Q.
+  envs_entails Δ' Q → envs_entails Δ (P → Q).
 Proof.
-  intros ?? HQ. rewrite envs_app_sound //=; simpl. apply impl_intro_l.
+  rewrite /envs_entails=> ?? HQ.
+  rewrite envs_app_sound //=; simpl. apply impl_intro_l.
   rewrite (_ : P = â–¡?false P) // (into_persistent false P).
   by rewrite right_id persistently_and_sep_l wand_elim_r.
 Qed.
 
-Lemma tac_impl_intro_drop Δ P Q : (Δ ⊢ Q) → Δ ⊢ P → Q.
-Proof. intros. apply impl_intro_l. by rewrite and_elim_r. Qed.
+Lemma tac_impl_intro_drop Δ P Q : envs_entails Δ Q → envs_entails Δ (P → Q).
+Proof. rewrite /envs_entails=> ?. apply impl_intro_l. by rewrite and_elim_r. Qed.
 
 Lemma tac_wand_intro Δ Δ' i P Q :
-  envs_app false (Esnoc Enil i P) Δ = Some Δ' → (Δ' ⊢ Q) → Δ ⊢ P -∗ Q.
+  envs_app false (Esnoc Enil i P) Δ = Some Δ' →
+  envs_entails Δ' Q → envs_entails Δ (P -∗ Q).
 Proof.
-  intros ? HQ. rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
+  rewrite /envs_entails=> ? HQ.
+  rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
 Qed.
 Lemma tac_wand_intro_persistent Δ Δ' i P P' Q :
   IntoPersistent false P P' →
   envs_app true (Esnoc Enil i P') Δ = Some Δ' →
-  (Δ' ⊢ Q) → Δ ⊢ P -∗ Q.
+  envs_entails Δ' Q → envs_entails Δ (P -∗ Q).
 Proof.
-  intros. rewrite envs_app_sound //; simpl.
+  rewrite /envs_entails => ?? <-. rewrite envs_app_sound //; simpl.
   rewrite right_id. by apply wand_mono.
 Qed.
-Lemma tac_wand_intro_drop Δ P Q : (Δ ⊢ Q) → Δ ⊢ P -∗ Q.
-Proof. intros. apply wand_intro_l. by rewrite sep_elim_r. Qed.
+Lemma tac_wand_intro_drop Δ P Q : envs_entails Δ Q → envs_entails Δ (P -∗ Q).
+Proof. rewrite /envs_entails=> <-. apply wand_intro_l. by rewrite sep_elim_r. Qed.
 
 (* This is pretty much [tac_specialize_assert] with [js:=[j]] and [tac_exact],
 but it is doing some work to keep the order of hypotheses preserved. *)
@@ -589,9 +626,9 @@ Lemma tac_specialize Δ Δ' Δ'' i p j q P1 P2 R Q :
   | false => envs_replace j q false (Esnoc Enil j P2) Δ'
              (* remove [i] and make [j] spatial *)
   end = Some Δ'' →
-  (Δ'' ⊢ Q) → Δ ⊢ Q.
+  envs_entails Δ'' Q → envs_entails Δ Q.
 Proof.
-  intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
+  rewrite /envs_entails. intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
   - rewrite envs_lookup_persistent_sound // envs_simple_replace_sound //; simpl.
     rewrite right_id assoc (into_wand _ R) /=. destruct q; simpl.
     + by rewrite persistently_wand persistent_persistently !wand_elim_r.
@@ -607,9 +644,9 @@ Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q neg js R P1 P2 P1' Q :
   ('(Δ1,Δ2) ← envs_split (if neg is true then Right else Left) js Δ';
     Δ2' ← envs_app false (Esnoc Enil j P2) Δ2;
     Some (Δ1,Δ2')) = Some (Δ1,Δ2') → (* does not preserve position of [j] *)
-  (Δ1 ⊢ P1') → (Δ2' ⊢ Q) → Δ ⊢ Q.
+  envs_entails Δ1 P1' → envs_entails Δ2' Q → envs_entails Δ Q.
 Proof.
-  intros [? ->]%envs_lookup_delete_Some ??? HP1 HQ.
+  rewrite /envs_entails. intros [? ->]%envs_lookup_delete_Some ??? HP1 HQ.
   destruct (envs_split _ _ _) as [[? Δ2]|] eqn:?; simplify_eq/=;
     destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
   rewrite envs_lookup_sound // envs_split_sound //.
@@ -619,18 +656,18 @@ Proof.
   by rewrite persistently_if_elim assoc !wand_elim_r.
 Qed.
 
-Lemma tac_unlock P Q : (P ⊢ Q) → P ⊢ locked Q.
+Lemma tac_unlock Δ Q : envs_entails Δ Q → envs_entails Δ (locked Q).
 Proof. by unlock. Qed.
 
 Lemma tac_specialize_frame Δ Δ' j q R P1 P2 P1' Q Q' :
   envs_lookup_delete j Δ = Some (q, R, Δ') →
   IntoWand false R P1 P2 →
   ElimModal P1' P1 Q Q →
-  (Δ' ⊢ P1' ∗ locked Q') →
+  envs_entails Δ' (P1' ∗ locked Q') →
   Q' = (P2 -∗ Q)%I →
-  Δ ⊢ Q.
+  envs_entails Δ Q.
 Proof.
-  intros [? ->]%envs_lookup_delete_Some ?? HPQ ->.
+  rewrite /envs_entails. intros [? ->]%envs_lookup_delete_Some ?? HPQ ->.
   rewrite envs_lookup_sound //. rewrite HPQ -lock.
   rewrite (into_wand _ R) assoc -(comm _ P1') -assoc persistently_if_elim.
   rewrite -{2}(elim_modal P1' P1 Q Q). apply sep_mono_r, wand_intro_l.
@@ -641,9 +678,9 @@ Lemma tac_specialize_assert_pure Δ Δ' j q R P1 P2 φ Q :
   envs_lookup j Δ = Some (q, R) →
   IntoWand false R P1 P2 → FromPure P1 φ →
   envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ' →
-  φ → (Δ' ⊢ Q) → Δ ⊢ Q.
+  φ → envs_entails Δ' Q → envs_entails Δ Q.
 Proof.
-  intros. rewrite envs_simple_replace_sound //; simpl.
+  rewrite /envs_entails=> ????? <-. rewrite envs_simple_replace_sound //; simpl.
   rewrite right_id (into_wand _ R) -(from_pure P1) pure_True //.
   by rewrite wand_True wand_elim_r.
 Qed.
@@ -652,11 +689,11 @@ Lemma tac_specialize_assert_persistent Δ Δ' Δ'' j q P1 P2 R Q :
   envs_lookup_delete j Δ = Some (q, R, Δ') →
   IntoWand false R P1 P2 → Persistent P1 →
   envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'' →
-  (Δ' ⊢ P1) → (Δ'' ⊢ Q) → Δ ⊢ Q.
+  envs_entails Δ' P1 → envs_entails Δ'' Q → envs_entails Δ Q.
 Proof.
-  intros [? ->]%envs_lookup_delete_Some ??? HP1 <-.
+  rewrite /envs_entails. intros [? ->]%envs_lookup_delete_Some ??? HP1 <-.
   rewrite envs_lookup_sound //.
-  rewrite -(idemp uPred_and (envs_delete _ _ _)).
+  rewrite -(idemp uPred_and (of_envs (envs_delete _ _ _))).
   rewrite {1}HP1 (persistent P1) persistently_and_sep_l assoc.
   rewrite envs_simple_replace_sound' //; simpl.
   rewrite right_id (into_wand _ R) (persistently_elim_if q) -persistently_if_sep wand_elim_l.
@@ -665,27 +702,28 @@ Qed.
 
 Lemma tac_specialize_persistent_helper Δ Δ' j q P R Q :
   envs_lookup j Δ = Some (q,P) →
-  (Δ ⊢ R) → Persistent R →
+  envs_entails Δ R → Persistent R →
   envs_replace j q true (Esnoc Enil j R) Δ = Some Δ' →
-  (Δ' ⊢ Q) → Δ ⊢ Q.
+  envs_entails Δ' Q → envs_entails Δ Q.
 Proof.
-  intros ? HR ?? <-.
-  rewrite -(idemp uPred_and Δ) {1}HR and_sep_l.
+  rewrite /envs_entails. intros ? HR ?? <-.
+  rewrite -(idemp uPred_and (of_envs Δ)) {1}HR and_sep_l.
   rewrite envs_replace_sound //; simpl.
   by rewrite right_id assoc (sep_elim_l R) persistent_persistently wand_elim_r.
 Qed.
 
 Lemma tac_revert Δ Δ' i p P Q :
   envs_lookup_delete i Δ = Some (p,P,Δ') →
-  (Δ' ⊢ (if p then □ P else P) -∗ Q) → Δ ⊢ Q.
+  envs_entails Δ' ((if p then □ P else P)%I -∗ Q) →
+  envs_entails Δ Q.
 Proof.
-  intros ? HQ. rewrite envs_lookup_delete_sound //; simpl.
+  rewrite /envs_entails=> ? HQ. rewrite envs_lookup_delete_sound //; simpl.
   by rewrite HQ /uPred_persistently_if wand_elim_r.
 Qed.
 
 Class IntoIH (φ : Prop) (Δ : envs M) (Q : uPred M) :=
-  into_ih : φ → Δ ⊢ Q.
-Global Instance into_ih_entails Δ Q : IntoIH (of_envs Δ ⊢ Q) Δ Q.
+  into_ih : φ → of_envs Δ ⊢ Q.
+Global Instance into_ih_entails Δ Q : IntoIH (envs_entails Δ Q) Δ Q.
 Proof. by rewrite /IntoIH. Qed.
 Global Instance into_ih_forall {A} (φ : A → Prop) Δ Φ :
   (∀ x, IntoIH (φ x) Δ (Φ x)) → IntoIH (∀ x, φ x) Δ (∀ x, Φ x) | 2.
@@ -697,20 +735,21 @@ Proof. rewrite /IntoIH=> HΔ ?. apply impl_intro_l, pure_elim_l. auto. Qed.
 Lemma tac_revert_ih Δ P Q {φ : Prop} (Hφ : φ) :
   IntoIH φ Δ P →
   env_spatial_is_nil Δ = true →
-  (of_envs Δ ⊢ □ P → Q) →
-  (of_envs Δ ⊢ Q).
+  envs_entails Δ (□ P → Q) →
+  envs_entails Δ Q.
 Proof.
-  rewrite /IntoIH. intros HP ? HPQ.
-  by rewrite -(idemp uPred_and Δ) {1}(persistent Δ) {1}HP // HPQ impl_elim_r.
+  rewrite /envs_entails /IntoIH=> HP ? HPQ.
+  rewrite -(idemp uPred_and (of_envs Δ)) {1}(persistent (of_envs Δ)).
+  by rewrite {1}HP // HPQ impl_elim_r.
 Qed.
 
 Lemma tac_assert Δ Δ1 Δ2 Δ2' neg js j P P' Q :
   ElimModal P' P Q Q →
   envs_split (if neg is true then Right else Left) js Δ = Some (Δ1,Δ2) →
   envs_app false (Esnoc Enil j P) Δ2 = Some Δ2' →
-  (Δ1 ⊢ P') → (Δ2' ⊢ Q) → Δ ⊢ Q.
+  envs_entails Δ1 P' → envs_entails Δ2' Q → envs_entails Δ Q.
 Proof.
-  intros ??? HP HQ. rewrite envs_split_sound //.
+  rewrite /envs_entails=> ??? HP HQ. rewrite envs_split_sound //.
   rewrite (envs_app_sound Δ2) //; simpl.
   by rewrite right_id HP HQ.
 Qed.
@@ -719,9 +758,10 @@ Lemma tac_assert_persistent Δ Δ1 Δ2 Δ' neg js j P Q :
   envs_split (if neg is true then Right else Left) js Δ = Some (Δ1,Δ2) →
   envs_app false (Esnoc Enil j P) Δ = Some Δ' →
   Persistent P →
-  (Δ1 ⊢ P) → (Δ' ⊢ Q) → Δ ⊢ Q.
+  envs_entails Δ1 P → envs_entails Δ' Q → envs_entails Δ Q.
 Proof.
-  intros ??? HP <-. rewrite -(idemp uPred_and Δ) {1}envs_split_sound //.
+  rewrite /envs_entails=> ??? HP <-.
+  rewrite -(idemp uPred_and (of_envs Δ)) {1}envs_split_sound //.
   rewrite HP sep_elim_l (and_sep_l P) envs_app_sound //; simpl.
   by rewrite right_id wand_elim_r.
 Qed.
@@ -729,27 +769,27 @@ Qed.
 Lemma tac_assert_pure Δ Δ' j P φ Q :
   envs_app false (Esnoc Enil j P) Δ = Some Δ' →
   FromPure P φ →
-  φ → (Δ' ⊢ Q) → Δ ⊢ Q.
+  φ → envs_entails Δ' Q → envs_entails Δ Q.
 Proof.
-  intros ??? <-. rewrite envs_app_sound //; simpl.
+  rewrite /envs_entails=> ??? <-. rewrite envs_app_sound //; simpl.
   by rewrite right_id -(from_pure P) pure_True // -impl_wand True_impl.
 Qed.
 
 Lemma tac_pose_proof Δ Δ' j P Q :
   P →
   envs_app true (Esnoc Enil j P) Δ = Some Δ' →
-  (Δ' ⊢ Q) → Δ ⊢ Q.
+  envs_entails Δ' Q → envs_entails Δ Q.
 Proof.
-  intros HP ? <-. rewrite envs_app_sound //; simpl.
+  rewrite /envs_entails=> HP ? <-. rewrite envs_app_sound //; simpl.
   by rewrite right_id -HP persistently_pure wand_True.
 Qed.
 
 Lemma tac_pose_proof_hyp Δ Δ' Δ'' i p j P Q :
   envs_lookup_delete i Δ = Some (p, P, Δ') →
   envs_app p (Esnoc Enil j P) (if p then Δ else Δ') = Some Δ'' →
-  (Δ'' ⊢ Q) → Δ ⊢ Q.
+  envs_entails Δ'' Q → envs_entails Δ Q.
 Proof.
-  intros [? ->]%envs_lookup_delete_Some ? <-. destruct p.
+  rewrite /envs_entails. intros [? ->]%envs_lookup_delete_Some ? <-. destruct p.
   - rewrite envs_lookup_persistent_sound // envs_app_sound //; simpl.
     by rewrite right_id wand_elim_r.
   - rewrite envs_lookup_sound // envs_app_sound //; simpl.
@@ -758,9 +798,9 @@ Qed.
 
 Lemma tac_apply Δ Δ' i p R P1 P2 :
   envs_lookup_delete i Δ = Some (p, R, Δ') → IntoWand false R P1 P2 →
-  (Δ' ⊢ P1) → Δ ⊢ P2.
+  envs_entails Δ' P1 → envs_entails Δ P2.
 Proof.
-  intros ?? HP1. rewrite envs_lookup_delete_sound' //.
+  rewrite /envs_entails=> ?? HP1. rewrite envs_lookup_delete_sound' //.
   by rewrite (into_wand _ R) HP1 wand_elim_l.
 Qed.
 
@@ -771,9 +811,10 @@ Lemma tac_rewrite Δ i p Pxy d Q :
     IntoInternalEq Pxy x y →
     (Q ⊣⊢ Φ (if d is Left then y else x)) →
     NonExpansive Φ →
-    (Δ ⊢ Φ (if d is Left then x else y)) → Δ ⊢ Q.
+    envs_entails Δ (Φ (if d is Left then x else y)) →
+    envs_entails Δ Q.
 Proof.
-  intros ? A x y Φ HPxy -> ? HΔ.
+  rewrite /envs_entails=> ? A x y Φ HPxy -> ? HΔ.
   rewrite -(idemp (∧)%I (of_envs Δ)) {1}envs_lookup_sound' //.
   rewrite sep_elim_l HPxy HΔ. apply impl_elim_l'. destruct d.
   - by apply internal_eq_rewrite.
@@ -788,9 +829,10 @@ Lemma tac_rewrite_in Δ i p Pxy j q P d Q :
     (P ⊣⊢ Φ (if d is Left then y else x)) →
     NonExpansive Φ →
     envs_simple_replace j q (Esnoc Enil j (Φ (if d is Left then x else y))) Δ = Some Δ' →
-    (Δ' ⊢ Q) → Δ ⊢ Q.
+    envs_entails Δ' Q →
+    envs_entails Δ Q.
 Proof.
-  intros ?? A Δ' x y Φ HPxy HP ?? <-.
+  rewrite /envs_entails=> ?? A Δ' x y Φ HPxy HP ?? <-.
   rewrite -(idemp uPred_and (of_envs Δ)) {2}(envs_lookup_sound' _ i) //.
   rewrite sep_elim_l HPxy and_sep_r.
   rewrite (envs_simple_replace_sound _ _ j) //; simpl.
@@ -803,16 +845,20 @@ Qed.
 
 (** * Conjunction splitting *)
 Lemma tac_and_split Δ P Q1 Q2 :
-  FromAnd true P Q1 Q2 → (Δ ⊢ Q1) → (Δ ⊢ Q2) → Δ ⊢ P.
-Proof. intros. rewrite -(from_and true P). by apply and_intro. Qed.
+  FromAnd true P Q1 Q2 →
+  envs_entails Δ Q1 → envs_entails Δ Q2 → envs_entails Δ P.
+Proof.
+  rewrite /envs_entails=> ???. rewrite -(from_and true P). by apply and_intro.
+Qed.
 
 (** * Separating conjunction splitting *)
 Lemma tac_sep_split Δ Δ1 Δ2 d js P Q1 Q2 :
   FromAnd false P Q1 Q2 →
   envs_split d js Δ = Some (Δ1,Δ2) →
-  (Δ1 ⊢ Q1) → (Δ2 ⊢ Q2) → Δ ⊢ P.
+  envs_entails Δ1 Q1 → envs_entails Δ2 Q2 → envs_entails Δ P.
 Proof.
-  intros. rewrite envs_split_sound // -(from_and false P). by apply sep_mono.
+  rewrite /envs_entails=> ????.
+  rewrite envs_split_sound // -(from_and false P). by apply sep_mono.
 Qed.
 
 (** * Combining *)
@@ -832,9 +878,9 @@ Lemma tac_combine Δ1 Δ2 Δ3 js p Ps j P Q :
   envs_lookup_delete_list js false Δ1 = Some (p, Ps, Δ2) →
   FromSeps P Ps →
   envs_app p (Esnoc Enil j P) Δ2 = Some Δ3 →
-  (Δ3 ⊢ Q) → Δ1 ⊢ Q.
+  envs_entails Δ3 Q → envs_entails Δ1 Q.
 Proof.
-  intros ??? <-. rewrite envs_lookup_delete_list_sound //.
+  rewrite /envs_entails=> ??? <-. rewrite envs_lookup_delete_list_sound //.
   rewrite from_seps. rewrite envs_app_sound //; simpl.
   by rewrite right_id wand_elim_r.
 Qed.
@@ -843,9 +889,10 @@ Qed.
 Lemma tac_and_destruct Δ Δ' i p j1 j2 P P1 P2 Q :
   envs_lookup i Δ = Some (p, P) → IntoAnd p P P1 P2 →
   envs_simple_replace i p (Esnoc (Esnoc Enil j1 P1) j2 P2) Δ = Some Δ' →
-  (Δ' ⊢ Q) → Δ ⊢ Q.
+  envs_entails Δ' Q → envs_entails Δ Q.
 Proof.
-  intros. rewrite envs_simple_replace_sound //; simpl. rewrite (into_and p P).
+  rewrite /envs_entails=> ??? <-.
+  rewrite envs_simple_replace_sound //; simpl. rewrite (into_and p P).
   by destruct p; rewrite /= ?right_id (comm _ P1) ?persistently_and_sep wand_elim_r.
 Qed.
 
@@ -855,9 +902,9 @@ to the principle of "external choice" in linear logic. *)
 Lemma tac_and_destruct_choice Δ Δ' i p d j P P1 P2 Q :
   envs_lookup i Δ = Some (p, P) → IntoAnd true P P1 P2 →
   envs_simple_replace i p (Esnoc Enil j (if d is Left then P1 else P2)) Δ = Some Δ' →
-  (Δ' ⊢ Q) → Δ ⊢ Q.
+  envs_entails Δ' Q → envs_entails Δ Q.
 Proof.
-  intros. rewrite envs_simple_replace_sound //; simpl.
+  rewrite /envs_entails=> ??? <-. rewrite envs_simple_replace_sound //; simpl.
   rewrite right_id (into_and true P). destruct d.
   - by rewrite and_elim_l wand_elim_r.
   - by rewrite and_elim_r wand_elim_r.
@@ -865,33 +912,40 @@ Qed.
 
 (** * Framing *)
 Lemma tac_frame_pure Δ (φ : Prop) P Q :
-  φ → Frame true ⌜φ⌝ P Q → (Δ ⊢ Q) → Δ ⊢ P.
+  φ → Frame true ⌜φ⌝ P Q → envs_entails Δ Q → envs_entails Δ P.
 Proof.
-  intros ?? ->. by rewrite -(frame ⌜φ⌝ P) /= persistently_pure pure_True // left_id.
+  rewrite /envs_entails=> ?? ->.
+  by rewrite -(frame ⌜φ⌝ P) /= persistently_pure pure_True // left_id.
 Qed.
 
 Lemma tac_frame Δ Δ' i p R P Q :
   envs_lookup_delete i Δ = Some (p, R, Δ') → Frame p R P Q →
-  ((if p then Δ else Δ') ⊢ Q) → Δ ⊢ P.
+  envs_entails (if p then Δ else Δ') Q → envs_entails Δ P.
 Proof.
-  intros [? ->]%envs_lookup_delete_Some ? HQ. destruct p.
+  rewrite /envs_entails. intros [? ->]%envs_lookup_delete_Some ? HQ. destruct p.
   - by rewrite envs_lookup_persistent_sound // -(frame R P) HQ.
   - rewrite envs_lookup_sound //; simpl. by rewrite -(frame R P) HQ.
 Qed.
 
 (** * Disjunction *)
-Lemma tac_or_l Δ P Q1 Q2 : FromOr P Q1 Q2 → (Δ ⊢ Q1) → Δ ⊢ P.
-Proof. intros. rewrite -(from_or P). by apply or_intro_l'. Qed.
-Lemma tac_or_r Δ P Q1 Q2 : FromOr P Q1 Q2 → (Δ ⊢ Q2) → Δ ⊢ P.
-Proof. intros. rewrite -(from_or P). by apply or_intro_r'. Qed.
+Lemma tac_or_l Δ P Q1 Q2 :
+  FromOr P Q1 Q2 → envs_entails Δ Q1 → envs_entails Δ P.
+Proof.
+  rewrite /envs_entails=> ? ->. 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 /envs_entails=> ? ->. rewrite -(from_or P). by apply or_intro_r'.
+Qed.
 
 Lemma tac_or_destruct Δ Δ1 Δ2 i p j1 j2 P P1 P2 Q :
   envs_lookup i Δ = Some (p, P) → IntoOr P P1 P2 →
   envs_simple_replace i p (Esnoc Enil j1 P1) Δ = Some Δ1 →
   envs_simple_replace i p (Esnoc Enil j2 P2) Δ = Some Δ2 →
-  (Δ1 ⊢ Q) → (Δ2 ⊢ Q) → Δ ⊢ Q.
+  envs_entails Δ1 Q → envs_entails Δ2 Q → envs_entails Δ Q.
 Proof.
-  intros ???? HP1 HP2. rewrite envs_lookup_sound //.
+  rewrite /envs_entails=> ???? HP1 HP2. rewrite envs_lookup_sound //.
   rewrite (into_or P) persistently_if_or sep_or_r; apply or_elim.
   - rewrite (envs_simple_replace_sound' _ Δ1) //.
     by rewrite /= right_id wand_elim_r.
@@ -902,53 +956,59 @@ Qed.
 (** * Forall *)
 Lemma tac_forall_intro {A} Δ (Φ : A → uPred M) Q :
   FromForall Q Φ →
-  (∀ a, Δ ⊢ Φ a) →
-  Δ ⊢ Q.
-Proof. rewrite /FromForall=> <-. apply forall_intro. Qed.
+  (∀ a, envs_entails Δ (Φ a)) →
+  envs_entails Δ Q.
+Proof. rewrite /envs_entails /FromForall=> <-. apply forall_intro. Qed.
 
 Lemma tac_forall_specialize {A} Δ Δ' i p P (Φ : A → uPred M) Q :
   envs_lookup i Δ = Some (p, P) → IntoForall P Φ →
   (∃ x : A,
     envs_simple_replace i p (Esnoc Enil i (Φ x)) Δ = Some Δ' ∧
-    (Δ' ⊢ Q)) →
-  Δ ⊢ Q.
+    envs_entails Δ' Q) →
+  envs_entails Δ Q.
 Proof.
-  intros ?? (x&?&?). rewrite envs_simple_replace_sound //; simpl.
+  rewrite /envs_entails. intros ?? (x&?&?).
+  rewrite envs_simple_replace_sound //; simpl.
   by rewrite right_id (into_forall P) (forall_elim x) wand_elim_r.
 Qed.
 
 Lemma tac_forall_revert {A} Δ (Φ : A → uPred M) :
-  (Δ ⊢ ∀ a, Φ a) → ∀ a, Δ ⊢ Φ a.
-Proof. intros HΔ a. by rewrite HΔ (forall_elim a). Qed.
+  envs_entails Δ (∀ a, Φ a) → ∀ a, envs_entails Δ (Φ a).
+Proof. rewrite /envs_entails=> HΔ a. by rewrite HΔ (forall_elim a). Qed.
 
 (** * Existential *)
 Lemma tac_exist {A} Δ P (Φ : A → uPred M) :
-  FromExist P Φ → (∃ a, Δ ⊢ Φ a) → Δ ⊢ P.
-Proof. intros ? [a ?]. rewrite -(from_exist P). eauto using exist_intro'. Qed.
+  FromExist P Φ → (∃ a, envs_entails Δ (Φ a)) → envs_entails Δ P.
+Proof.
+  rewrite /envs_entails=> ? [a ?].
+  rewrite -(from_exist P). eauto using exist_intro'.
+Qed.
 
 Lemma tac_exist_destruct {A} Δ i p j P (Φ : A → uPred M) Q :
   envs_lookup i Δ = Some (p, P) → IntoExist P Φ →
   (∀ a, ∃ Δ',
-    envs_simple_replace i p (Esnoc Enil j (Φ a)) Δ = Some Δ' ∧ (Δ' ⊢ Q)) →
-  Δ ⊢ Q.
+    envs_simple_replace i p (Esnoc Enil j (Φ a)) Δ = Some Δ' ∧
+    envs_entails Δ' Q) →
+  envs_entails Δ Q.
 Proof.
-  intros ?? HΦ. rewrite envs_lookup_sound //.
+  rewrite /envs_entails=> ?? HΦ. rewrite envs_lookup_sound //.
   rewrite (into_exist P) persistently_if_exist sep_exist_r.
   apply exist_elim=> a; destruct (HΦ a) as (Δ'&?&?).
   rewrite envs_simple_replace_sound' //; simpl. by rewrite right_id wand_elim_r.
 Qed.
 
 (** * Modalities *)
-Lemma tac_modal_intro Δ P Q : FromModal P Q → (Δ ⊢ Q) → Δ ⊢ P.
-Proof. rewrite /FromModal. by intros <- ->. Qed.
+Lemma tac_modal_intro Δ P Q :
+  FromModal P Q → envs_entails Δ Q → envs_entails Δ P.
+Proof. by rewrite /envs_entails /FromModal=> <- ->. Qed.
 
 Lemma tac_modal_elim Δ Δ' i p P' P Q Q' :
   envs_lookup i Δ = Some (p, P) →
   ElimModal P P' Q Q' →
   envs_replace i p false (Esnoc Enil i P') Δ = Some Δ' →
-  (Δ' ⊢ Q') → Δ ⊢ Q.
+  envs_entails Δ' Q' → envs_entails Δ Q.
 Proof.
-  intros ??? HΔ. rewrite envs_replace_sound //; simpl.
+  rewrite /envs_entails=> ??? HΔ. rewrite envs_replace_sound //; simpl.
   rewrite right_id HΔ persistently_if_elim. by apply elim_modal.
 Qed.
 End tactics.
diff --git a/theories/proofmode/notation.v b/theories/proofmode/notation.v
index 8e34280a8..bf7dd0f00 100644
--- a/theories/proofmode/notation.v
+++ b/theories/proofmode/notation.v
@@ -11,18 +11,19 @@ Notation "" := Enil (only printing) : proof_scope.
 Notation "Γ H : P" := (Esnoc Γ H P)
   (at level 1, P at level 200,
    left associativity, format "Γ H  :  P '//'", only printing) : proof_scope.
+
 Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q" :=
-  (of_envs (Envs Γ Δ) ⊢ Q%I)
+  (envs_entails (Envs Γ Δ) Q%I)
   (at level 1, Q at level 200, left associativity,
   format "Γ '--------------------------------------' □ '//' Δ '--------------------------------------' ∗ '//' Q '//'", only printing) :
   C_scope.
 Notation "Δ '--------------------------------------' ∗ Q" :=
-  (of_envs (Envs Enil Δ) ⊢ Q%I)
+  (envs_entails (Envs Enil Δ) Q%I)
   (at level 1, Q at level 200, left associativity,
   format "Δ '--------------------------------------' ∗ '//' Q '//'", only printing) : C_scope.
 Notation "Γ '--------------------------------------' □ Q" :=
-  (of_envs (Envs Γ Enil) ⊢ Q%I)
+  (envs_entails (Envs Γ Enil) Q%I)
   (at level 1, Q at level 200, left associativity,
   format "Γ '--------------------------------------' □ '//' Q '//'", only printing)  : C_scope.
-Notation "'--------------------------------------' ∗ Q" := (of_envs (Envs Enil Enil) ⊢ Q%I)
+Notation "'--------------------------------------' ∗ Q" := (envs_entails (Envs Enil Enil) Q%I)
   (at level 1, Q at level 200, format "'--------------------------------------' ∗ '//' Q '//'", only printing) : C_scope.
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index fd39e7ff2..7ea207f4c 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -1,6 +1,6 @@
 From iris.proofmode Require Import coq_tactics.
 From iris.proofmode Require Import base intro_patterns spec_patterns sel_patterns.
-From iris.base_logic Require Export base_logic.
+From iris.base_logic Require Export base_logic big_op.
 From iris.proofmode Require Export classes notation.
 From iris.proofmode Require Import class_instances.
 From stdpp Require Import stringmap hlist.
@@ -22,7 +22,7 @@ Ltac env_reflexivity := env_cbv; exact eq_refl.
 (* Tactic Notation tactics cannot return terms *)
 Ltac iFresh' H :=
   lazymatch goal with
-  |- of_envs ?Δ ⊢ _ =>
+  |- envs_entails ?Δ _ =>
      (* [vm_compute fails] if any of the hypotheses in [Δ] contain evars, so
      first use [cbv] to compute the domain of [Δ] *)
      let Hs := eval cbv in (envs_dom Δ) in
@@ -34,14 +34,14 @@ Ltac iFresh := iFresh' "~".
 Ltac iMissingHyps Hs :=
   let Δ :=
     lazymatch goal with
-    | |- of_envs ?Δ ⊢ _ => Δ
+    | |- envs_entails ?Δ _ => Δ
     | |- context[ envs_split _ _ ?Δ ] => Δ
     end in
   let Hhyps := eval env_cbv in (envs_dom Δ) in
   eval vm_compute in (list_difference Hs Hhyps).
 
 Ltac iTypeOf H :=
-  let Δ := match goal with |- of_envs ?Δ ⊢ _ => Δ end in
+  let Δ := match goal with |- envs_entails ?Δ _ => Δ end in
   eval env_cbv in (envs_lookup H Δ).
 
 Tactic Notation "iMatchHyp" tactic1(tac) :=
@@ -64,7 +64,7 @@ Proof. split. apply uPred.equiv_iff. apply uPred.iff_equiv. Qed.
 (** * Start a proof *)
 Ltac iStartProof :=
   lazymatch goal with
-  | |- of_envs _ ⊢ _ => idtac
+  | |- envs_entails _ _ => idtac
   | |- ?P =>
     apply (proj2 (_ : AsValid P _)), tac_adequate
     || fail "iStartProof: not a uPred"
@@ -100,7 +100,7 @@ Ltac iElaborateSelPat pat :=
        end
     end in
   lazymatch goal with
-  | |- of_envs ?Δ ⊢ _ =>
+  | |- envs_entails ?Δ _ =>
     let pat := sel_pat.parse pat in go pat Δ (@nil esel_pat)
   end.
 
@@ -152,7 +152,7 @@ Tactic Notation "iAssumption" :=
        |find p Γ Q]
     end in
   match goal with
-  | |- of_envs (Envs ?Γp ?Γs) ⊢ ?Q =>
+  | |- envs_entails (Envs ?Γp ?Γs) ?Q =>
      first [find true Γp Q | find false Γs Q
            |fail "iAssumption:" Q "not found"]
   end.
@@ -189,7 +189,7 @@ Tactic Notation "iPureIntro" :=
 Local Ltac iFrameFinish :=
   lazy iota beta;
   try match goal with
-  | |- _ ⊢ True => exact (uPred.pure_intro _ _ I)
+  | |- envs_entails _ True => exact (uPred.pure_intro _ _ I)
   end.
 
 Local Ltac iFramePure t :=
@@ -213,7 +213,7 @@ Local Ltac iFrameAnyPersistent :=
   let rec go Hs :=
     match Hs with [] => idtac | ?H :: ?Hs => repeat iFrameHyp H; go Hs end in
   match goal with
-  | |- of_envs ?Δ ⊢ _ =>
+  | |- envs_entails ?Δ _ =>
      let Hs := eval cbv in (env_dom (env_persistent Δ)) in go Hs
   end.
 
@@ -221,7 +221,7 @@ Local Ltac iFrameAnySpatial :=
   let rec go Hs :=
     match Hs with [] => idtac | ?H :: ?Hs => try iFrameHyp H; go Hs end in
   match goal with
-  | |- of_envs ?Δ ⊢ _ =>
+  | |- envs_entails ?Δ _ =>
      let Hs := eval cbv in (env_dom (env_spatial Δ)) in go Hs
   end.
 
@@ -284,7 +284,7 @@ Tactic Notation "iFrame" "(" constr(t1) constr(t2) constr(t3) constr(t4)
 Local Tactic Notation "iIntro" "(" simple_intropattern(x) ")" :=
   try iStartProof;
   lazymatch goal with
-  | |- _ ⊢ _ =>
+  | |- envs_entails _ _ =>
     eapply tac_forall_intro;
       [apply _ ||
        let P := match goal with |- FromForall ?P _ => P end in
@@ -342,14 +342,14 @@ Local Tactic Notation "iIntroForall" :=
   lazymatch goal with
   | |- ∀ _, ?P => fail
   | |- ∀ _, _ => intro
-  | |- _ ⊢ (∀ x : _, _) => let x' := fresh x in iIntro (x')
+  | |- envs_entails _ (∀ x : _, _) => let x' := fresh x in iIntro (x')
   end.
 Local Tactic Notation "iIntro" :=
   try iStartProof;
   lazymatch goal with
   | |- _ → ?P => intro
-  | |- _ ⊢ (_ -∗ _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H
-  | |- _ ⊢ (_ → _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H
+  | |- envs_entails _ (_ -∗ _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H
+  | |- envs_entails _ (_ → _) => iIntro (?) || let H := iFresh in iIntro #H || iIntro H
   end.
 
 (** * Specialize *)
@@ -692,13 +692,10 @@ Local Tactic Notation "iOrDestruct" constr(H) "as" constr(H1) constr(H2) :=
 (** * Conjunction and separating conjunction *)
 Tactic Notation "iSplit" :=
   iStartProof;
-  lazymatch goal with
-  | |- _ ⊢ _ =>
-    eapply tac_and_split;
-      [apply _ ||
-       let P := match goal with |- FromAnd _ ?P _ _ => P end in
-       fail "iSplit:" P "not a conjunction"| |]
-  end.
+  eapply tac_and_split;
+    [apply _ ||
+     let P := match goal with |- FromAnd _ ?P _ _ => P end in
+     fail "iSplit:" P "not a conjunction"| |].
 
 Tactic Notation "iSplitL" constr(Hs) :=
   iStartProof;
@@ -809,7 +806,7 @@ Tactic Notation "iAlways":=
 (** * Later *)
 Tactic Notation "iNext" open_constr(n) :=
   iStartProof;
-  let P := match goal with |- _ ⊢ ?P => P end in
+  let P := match goal with |- envs_entails _ ?P => P end in
   try lazymatch n with 0 => fail 1 "iNext: cannot strip 0 laters" end;
   eapply (tac_next _ _ n);
     [apply _ || fail "iNext:" P "does not contain" n "laters"
@@ -1357,7 +1354,7 @@ result in the following actions:
 Tactic Notation "iInductionCore" constr(x) "as" simple_intropattern(pat) constr(IH) :=
   let rec fix_ihs :=
     lazymatch goal with
-    | H : context [coq_tactics.of_envs _ ⊢ _] |- _ =>
+    | H : context [envs_entails _ _] |- _ =>
        eapply (tac_revert_ih _ _ _ H _);
          [reflexivity
           || fail "iInduction: spatial context not empty, this should not happen"|];
@@ -1377,8 +1374,8 @@ Ltac iHypsContaining x :=
        | _ => go Γ x Hs
        end
      end in
-  let Γp := lazymatch goal with |- of_envs (Envs ?Γp _) ⊢ _ => Γp end in
-  let Γs := lazymatch goal with |- of_envs (Envs _ ?Γs) ⊢ _ => Γs end in
+  let Γp := lazymatch goal with |- envs_entails (Envs ?Γp _) _ => Γp end in
+  let Γs := lazymatch goal with |- envs_entails (Envs _ ?Γs) _ => Γs end in
   let Hs := go Γp x (@nil string) in go Γs x Hs.
 
 Tactic Notation "iInductionRevert" constr(x) constr(Hs) "with" tactic(tac) :=
@@ -1703,24 +1700,33 @@ Tactic Notation "iMod" open_constr(lem) "as" "(" simple_intropattern(x1)
 Tactic Notation "iMod" open_constr(lem) "as" "%" simple_intropattern(pat) :=
   iDestructCore lem as false (fun H => iModCore H; iPure H as pat).
 
+Hint Extern 0 (_ ⊢ _) => iStartProof.
+
 (* Make sure that by and done solve trivial things in proof mode *)
-Hint Extern 0 (of_envs _ ⊢ _) => by iPureIntro.
-Hint Extern 0 (of_envs _ ⊢ _) => iAssumption.
-Hint Resolve uPred.internal_eq_refl'. (* Maybe make an [iReflexivity] tactic *)
-
-(* For iIntros we do not check whether we are in proof mode because we actually
-want it to enter proof mode when we are not already in it. *)
-Hint Extern 0 (_ ⊢ _) => progress iIntros.
-
-Hint Extern 1 (of_envs _ ⊢ _ ∧ _) => iSplit.
-Hint Extern 1 (of_envs _ ⊢ _ ∗ _) => iSplit.
-Hint Extern 1 (of_envs _ ⊢ ▷ _) => iNext.
-Hint Extern 1 (of_envs _ ⊢ □ _) => iAlways.
-Hint Extern 1 (of_envs _ ⊢ ■ _) => iAlways.
-Hint Extern 1 (of_envs _ ⊢ ∃ _, _) => iExists _.
-Hint Extern 1 (of_envs _ ⊢ |==> _) => iModIntro.
-Hint Extern 1 (of_envs _ ⊢ ◇ _) => iModIntro.
-Hint Extern 1 (of_envs _ ⊢ _ ∨ _) => iLeft.
-Hint Extern 1 (of_envs _ ⊢ _ ∨ _) => iRight.
-
-Hint Extern 2 (of_envs _ ⊢ _ ∗ _) => progress iFrame : iFrame.
+Hint Extern 0 (envs_entails _ _) => iPureIntro; try done.
+Hint Extern 0 (envs_entails _ _) => iAssumption.
+
+(* TODO: look for a more principled way of adding trivial hints like those
+below; see the discussion in !75 for further details. *)
+Hint Extern 0 (envs_entails _ (_ ≡ _)) => apply uPred.internal_eq_refl'.
+Hint Extern 0 (envs_entails _ (big_opL _ _ _)) => apply big_sepL_nil'.
+Hint Extern 0 (envs_entails _ (big_opM _ _ _)) => apply big_sepM_empty'.
+Hint Extern 0 (envs_entails _ (big_opS _ _ _)) => apply big_sepS_empty'.
+Hint Extern 0 (envs_entails _ (big_opMS _ _ _)) => apply big_sepMS_empty'.
+
+Hint Extern 0 (envs_entails _ (∀ _, _)) => iIntros.
+Hint Extern 0 (envs_entails _ (_ → _)) => iIntros.
+Hint Extern 0 (envs_entails _ (_ -∗ _)) => iIntros.
+
+Hint Extern 1 (envs_entails _ (_ ∧ _)) => iSplit.
+Hint Extern 1 (envs_entails _ (_ ∗ _)) => iSplit.
+Hint Extern 1 (envs_entails _ (â–· _)) => iNext.
+Hint Extern 1 (envs_entails _ (â–¡ _)) => iAlways.
+Hint Extern 1 (envs_entails _ (â–  _)) => iAlways.
+Hint Extern 1 (envs_entails _ (∃ _, _)) => iExists _.
+Hint Extern 1 (envs_entails _ (|==> _)) => iModIntro.
+Hint Extern 1 (envs_entails _ (â—‡ _)) => iModIntro.
+Hint Extern 1 (envs_entails _ (_ ∨ _)) => iLeft.
+Hint Extern 1 (envs_entails _ (_ ∨ _)) => iRight.
+
+Hint Extern 2 (envs_entails _ (_ ∗ _)) => progress iFrame : iFrame.
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 2ca6c7bf3..748c19512 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -144,7 +144,7 @@ Qed.
 
 Lemma test_eauto_iFramE P Q R `{!Persistent R} :
   P -∗ Q -∗ R -∗ R ∗ Q ∗ P ∗ R ∨ False.
-Proof. eauto with iFrame. Qed.
+Proof. eauto 10 with iFrame. Qed.
 
 Lemma test_iCombine_persistent P Q R `{!Persistent R} :
   P -∗ Q -∗ R -∗ R ∗ Q ∗ P ∗ R ∨ False.
-- 
GitLab