From 0ca74ec7042ffd18e75481cf9e09cb5c98580de6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 18 May 2021 00:55:23 +0200
Subject: [PATCH] Remove useless scopes. Thanks to !674.

---
 iris/base_logic/algebra.v                  |  4 ++--
 iris/base_logic/bupd_alt.v                 |  2 +-
 iris/base_logic/derived.v                  |  4 ++--
 iris/base_logic/lib/boxes.v                |  2 +-
 iris/base_logic/lib/gen_inv_heap.v         |  6 ++---
 iris/base_logic/lib/na_invariants.v        |  4 ++--
 iris/base_logic/lib/proph_map.v            |  4 ++--
 iris/base_logic/lib/wsat.v                 |  1 -
 iris/bi/big_op.v                           | 20 ++++++++---------
 iris/bi/derived_connectives.v              | 14 ++++++------
 iris/bi/derived_laws.v                     | 10 ++++-----
 iris/bi/derived_laws_later.v               | 12 +++++-----
 iris/bi/lib/atomic.v                       |  5 ++---
 iris/bi/lib/core.v                         |  2 +-
 iris/bi/lib/counterexamples.v              | 14 +++++-------
 iris/bi/lib/laterable.v                    |  2 +-
 iris/bi/lib/relations.v                    |  2 +-
 iris/bi/monpred.v                          | 12 +++++-----
 iris/bi/plainly.v                          | 14 ++++++------
 iris/bi/updates.v                          | 14 ++++++------
 iris/program_logic/atomic.v                |  6 ++---
 iris/program_logic/total_adequacy.v        |  4 ++--
 iris/proofmode/class_instances.v           | 14 ++++++------
 iris/proofmode/class_instances_embedding.v |  4 ++--
 iris/proofmode/class_instances_later.v     | 26 +++++++++++-----------
 iris/proofmode/class_instances_plainly.v   |  2 +-
 iris/proofmode/class_instances_updates.v   |  6 ++---
 iris/proofmode/coq_tactics.v               | 16 ++++++-------
 iris/proofmode/frame_instances.v           |  4 ++--
 iris/proofmode/monpred.v                   | 10 ++++-----
 30 files changed, 118 insertions(+), 122 deletions(-)

diff --git a/iris/base_logic/algebra.v b/iris/base_logic/algebra.v
index ead999ce2..138969cfc 100644
--- a/iris/base_logic/algebra.v
+++ b/iris/base_logic/algebra.v
@@ -10,7 +10,7 @@ Section upred.
 Context {M : ucmra}.
 
 (* Force implicit argument M *)
-Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
+Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P Q).
 Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
 
 Lemma prod_validI {A B : cmra} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
@@ -146,7 +146,7 @@ Section view.
   Qed.
   Lemma view_both_dfrac_validI_2 (relI : uPred M) dq a b :
     (∀ n (x : M), relI n x → rel n a b) →
-    ⌜✓dq⌝%Qp ∧ relI ⊢ ✓ (●V{dq} a ⋅ ◯V b : view rel).
+    ⌜✓dq⌝ ∧ relI ⊢ ✓ (●V{dq} a ⋅ ◯V b : view rel).
   Proof.
     intros Hrel. uPred.unseal. split=> n x _ /=.
     rewrite /uPred_holds /= view_both_dfrac_validN. by move=> [? /Hrel].
diff --git a/iris/base_logic/bupd_alt.v b/iris/base_logic/bupd_alt.v
index 5c6868233..e97df5dd1 100644
--- a/iris/base_logic/bupd_alt.v
+++ b/iris/base_logic/bupd_alt.v
@@ -8,7 +8,7 @@ Set Default Proof Using "Type*".
 (** This file contains an alternative version of basic updates, that is
 expression in terms of just the plain modality [â– ]. *)
 Definition bupd_alt `{BiPlainly PROP} (P : PROP) : PROP :=
-  (∀ R, (P -∗ ■ R) -∗ ■ R)%I.
+  ∀ R, (P -∗ ■ R) -∗ ■ R.
 
 (** This definition is stated for any BI with a plain modality. The above
 definition is akin to the continuation monad, where one should think of [â–  R]
diff --git a/iris/base_logic/derived.v b/iris/base_logic/derived.v
index b81a3b475..6b92ded31 100644
--- a/iris/base_logic/derived.v
+++ b/iris/base_logic/derived.v
@@ -15,7 +15,7 @@ Implicit Types P Q : uPred M.
 Implicit Types A : Type.
 
 (* Force implicit argument M *)
-Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
+Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P Q).
 Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
 
 (** Propers *)
@@ -24,7 +24,7 @@ Global Instance cmra_valid_proper {A : cmra} :
   Proper ((≡) ==> (⊣⊢)) (@uPred_cmra_valid M A) := ne_proper _.
 
 (** Own and valid derived *)
-Lemma persistently_cmra_valid_1 {A : cmra} (a : A) : ✓ a ⊢ <pers> (✓ a : uPred M).
+Lemma persistently_cmra_valid_1 {A : cmra} (a : A) : ✓ a ⊢@{uPredI M} <pers> (✓ a).
 Proof. by rewrite {1}plainly_cmra_valid_1 plainly_elim_persistently. Qed.
 Lemma intuitionistically_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
 Proof.
diff --git a/iris/base_logic/lib/boxes.v b/iris/base_logic/lib/boxes.v
index 56fb406b6..ca565ab8c 100644
--- a/iris/base_logic/lib/boxes.v
+++ b/iris/base_logic/lib/boxes.v
@@ -292,7 +292,7 @@ Proof.
   - iMod (slice_delete_full with "Hslice1 Hbox") as (P1) "(HQ1 & Heq1 & Hbox)"; try done.
     iMod (slice_delete_full with "Hslice2 Hbox") as (P2) "(HQ2 & Heq2 & Hbox)"; first done.
     { by simplify_map_eq. }
-    iMod (slice_insert_full _ _ _ _ (Q1 ∗ Q2)%I with "[$HQ1 $HQ2] Hbox")
+    iMod (slice_insert_full _ _ _ _ (Q1 ∗ Q2) with "[$HQ1 $HQ2] Hbox")
       as (γ ?) "[#Hslice Hbox]"; first done.
     iExists γ. iIntros "{$% $#} !>". iNext.
     iApply (internal_eq_rewrite_contractive _ _ (box _ _) with "[Heq1 Heq2] Hbox").
diff --git a/iris/base_logic/lib/gen_inv_heap.v b/iris/base_logic/lib/gen_inv_heap.v
index 87f3719df..ecb038af2 100644
--- a/iris/base_logic/lib/gen_inv_heap.v
+++ b/iris/base_logic/lib/gen_inv_heap.v
@@ -53,9 +53,9 @@ Section definitions.
   Context `{!invG Σ, !gen_heapG L V Σ, gG: !inv_heapG L V Σ}.
 
   Definition inv_heap_inv_P : iProp Σ :=
-    (∃ h : gmap L (V * (V -d> PropO)),
-        own (inv_heap_name gG) (● to_inv_heap h) ∗
-        [∗ map] l ↦ p ∈ h, ⌜p.2 p.1⌝ ∗ l ↦ p.1)%I.
+    ∃ h : gmap L (V * (V -d> PropO)),
+       own (inv_heap_name gG) (● to_inv_heap h) ∗
+       [∗ map] l ↦ p ∈ h, ⌜p.2 p.1⌝ ∗ l ↦ p.1.
 
   Definition inv_heap_inv : iProp Σ := inv inv_heapN inv_heap_inv_P.
 
diff --git a/iris/base_logic/lib/na_invariants.v b/iris/base_logic/lib/na_invariants.v
index 71131cf03..d4858462d 100644
--- a/iris/base_logic/lib/na_invariants.v
+++ b/iris/base_logic/lib/na_invariants.v
@@ -22,8 +22,8 @@ Section defs.
     own p (CoPset E, GSet ∅).
 
   Definition na_inv (p : na_inv_pool_name) (N : namespace) (P : iProp Σ) : iProp Σ :=
-    (∃ i, ⌜i ∈ (↑N:coPset)⌝ ∧
-          inv N (P ∗ own p (CoPset ∅, GSet {[i]}) ∨ na_own p {[i]}))%I.
+    ∃ i, ⌜i ∈ (↑N:coPset)⌝ ∧
+         inv N (P ∗ own p (CoPset ∅, GSet {[i]}) ∨ na_own p {[i]}).
 End defs.
 
 Global Instance: Params (@na_inv) 3 := {}.
diff --git a/iris/base_logic/lib/proph_map.v b/iris/base_logic/lib/proph_map.v
index 59848fa92..121e42e62 100644
--- a/iris/base_logic/lib/proph_map.v
+++ b/iris/base_logic/lib/proph_map.v
@@ -43,8 +43,8 @@ Section definitions.
     map_Forall (λ p vs, vs = proph_list_resolves pvs p) R.
 
   Definition proph_map_interp pvs (ps : gset P) : iProp Σ :=
-    (∃ R, ⌜proph_resolves_in_list R pvs ∧
-          dom (gset _) R ⊆ ps⌝ ∗ ghost_map_auth (proph_map_name pG) 1 R)%I.
+    ∃ R, ⌜proph_resolves_in_list R pvs ∧
+         dom (gset _) R ⊆ ps⌝ ∗ ghost_map_auth (proph_map_name pG) 1 R.
 
   Definition proph_def (p : P) (vs : list V) : iProp Σ :=
     p ↪[proph_map_name pG] vs.
diff --git a/iris/base_logic/lib/wsat.v b/iris/base_logic/lib/wsat.v
index 37ddb62df..bbfc5a9e9 100644
--- a/iris/base_logic/lib/wsat.v
+++ b/iris/base_logic/lib/wsat.v
@@ -35,7 +35,6 @@ Definition invariant_unfold {Σ} (P : iProp Σ) : later (iProp Σ) :=
   Next P.
 Definition ownI `{!invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
   own invariant_name (gmap_view_frag i DfracDiscarded (invariant_unfold P)).
-Global Arguments ownI {_ _} _ _%I.
 Typeclasses Opaque ownI.
 Global Instance: Params (@invariant_unfold) 1 := {}.
 Global Instance: Params (@ownI) 3 := {}.
diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 824da80c2..e7b702f29 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -718,7 +718,7 @@ Section sep_list2.
   Lemma big_sepL2_later_1 `{BiAffine PROP} Φ l1 l2 :
     (▷ [∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ⊢ ◇ [∗ list] k↦y1;y2 ∈ l1;l2, ▷ Φ k y1 y2.
   Proof.
-    rewrite !big_sepL2_alt later_and big_sepL_later (timeless ⌜ _ ⌝%I).
+    rewrite !big_sepL2_alt later_and big_sepL_later (timeless ⌜ _ ⌝).
     rewrite except_0_and. auto using and_mono, except_0_intro.
   Qed.
 
@@ -1189,7 +1189,7 @@ Section map.
     □ (∀ k x, ⌜m !! k = Some x⌝ → Φ k x) ⊢ [∗ map] k↦x ∈ m, Φ k x.
   Proof.
     revert Φ. induction m as [|i x m ? IH] using map_ind=> Φ.
-    { by rewrite (affine (â–¡ _)%I) big_sepM_empty. }
+    { by rewrite (affine (â–¡ _)) big_sepM_empty. }
     rewrite big_sepM_insert // intuitionistically_sep_dup. f_equiv.
     - rewrite (forall_elim i) (forall_elim x) lookup_insert.
       by rewrite pure_True // True_impl intuitionistically_elim.
@@ -1597,11 +1597,11 @@ Section map2.
     ⊣⊢ ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) ∗ ([∗ map] k↦y1;y2 ∈ m1;m2, Ψ k y1 y2).
   Proof.
     rewrite big_sepM2_eq /big_sepM2_def.
-    rewrite -{1}(and_idem ⌜∀ k : K, is_Some (m1 !! k) ↔ is_Some (m2 !! k)⌝%I).
-    rewrite -and_assoc.
+    rewrite -{1}(idemp bi_and ⌜∀ k : K, is_Some (m1 !! k) ↔ is_Some (m2 !! k)⌝%I).
+    rewrite -assoc.
     rewrite !persistent_and_affinely_sep_l /=.
-    rewrite -sep_assoc. apply sep_proper=>//.
-    rewrite sep_assoc (sep_comm _ (<affine> _)%I) -sep_assoc.
+    rewrite -assoc. apply sep_proper=>//.
+    rewrite assoc (comm _ _ (<affine> _)%I) -assoc.
     apply sep_proper=>//. apply big_sepM_sep.
   Qed.
 
@@ -1694,7 +1694,7 @@ Section map2.
     (▷ [∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2)
     ⊢ ◇ ([∗ map] k↦x1;x2 ∈ m1;m2, ▷ Φ k x1 x2).
   Proof.
-    rewrite big_sepM2_eq /big_sepM2_def later_and (timeless ⌜_⌝%I).
+    rewrite big_sepM2_eq /big_sepM2_def later_and (timeless ⌜_⌝).
     rewrite big_sepM_later except_0_and.
     auto using and_mono_r, except_0_intro.
   Qed.
@@ -1702,7 +1702,7 @@ Section map2.
     ([∗ map] k↦x1;x2 ∈ m1;m2, ▷ Φ k x1 x2)
     ⊢ ▷ [∗ map] k↦x1;x2 ∈ m1;m2, Φ k x1 x2.
   Proof.
-    rewrite big_sepM2_eq /big_sepM2_def later_and -(later_intro ⌜_⌝%I).
+    rewrite big_sepM2_eq /big_sepM2_def later_and -(later_intro ⌜_⌝).
     apply and_mono_r. by rewrite big_opM_commute.
   Qed.
 
@@ -1904,7 +1904,7 @@ Section gset.
     □ (∀ x, ⌜x ∈ X⌝ → Φ x) ⊢ [∗ set] x ∈ X, Φ x.
   Proof.
     revert Φ. induction X as [|x X ? IH] using set_ind_L=> Φ.
-    { by rewrite (affine (â–¡ _)%I) big_sepS_empty. }
+    { by rewrite (affine (â–¡ _)) big_sepS_empty. }
     rewrite intuitionistically_sep_dup big_sepS_insert //. f_equiv.
     - rewrite (forall_elim x) pure_True ?True_impl; last set_solver.
       by rewrite intuitionistically_elim.
@@ -2100,7 +2100,7 @@ Section gmultiset.
     □ (∀ x, ⌜x ∈ X⌝ → Φ x) ⊢ [∗ mset] x ∈ X, Φ x.
   Proof.
     revert Φ. induction X as [|x X IH] using gmultiset_ind=> Φ.
-    { by rewrite (affine (â–¡ _)%I) big_sepMS_empty. }
+    { by rewrite (affine (â–¡ _)) big_sepMS_empty. }
     rewrite intuitionistically_sep_dup big_sepMS_disj_union.
     rewrite big_sepMS_singleton. f_equiv.
     - rewrite (forall_elim x) pure_True ?True_impl; last multiset_solver.
diff --git a/iris/bi/derived_connectives.v b/iris/bi/derived_connectives.v
index 0c8ac604a..0027f0f0d 100644
--- a/iris/bi/derived_connectives.v
+++ b/iris/bi/derived_connectives.v
@@ -2,13 +2,13 @@ From iris.algebra Require Import monoid.
 From iris.bi Require Export interface.
 From iris.prelude Require Import options.
 
-Definition bi_iff {PROP : bi} (P Q : PROP) : PROP := ((P → Q) ∧ (Q → P))%I.
+Definition bi_iff {PROP : bi} (P Q : PROP) : PROP := (P → Q) ∧ (Q → P).
 Global Arguments bi_iff {_} _%I _%I : simpl never.
 Global Instance: Params (@bi_iff) 1 := {}.
 Infix "↔" := bi_iff : bi_scope.
 
 Definition bi_wand_iff {PROP : bi} (P Q : PROP) : PROP :=
-  ((P -∗ Q) ∧ (Q -∗ P))%I.
+  (P -∗ Q) ∧ (Q -∗ P).
 Global Arguments bi_wand_iff {_} _%I _%I : simpl never.
 Global Instance: Params (@bi_wand_iff) 1 := {}.
 Infix "∗-∗" := bi_wand_iff : bi_scope.
@@ -19,7 +19,7 @@ Global Arguments persistent {_} _%I {_}.
 Global Hint Mode Persistent + ! : typeclass_instances.
 Global Instance: Params (@Persistent) 1 := {}.
 
-Definition bi_affinely {PROP : bi} (P : PROP) : PROP := (emp ∧ P)%I.
+Definition bi_affinely {PROP : bi} (P : PROP) : PROP := emp ∧ P.
 Global Arguments bi_affinely {_} _%I : simpl never.
 Global Instance: Params (@bi_affinely) 1 := {}.
 Typeclasses Opaque bi_affinely.
@@ -38,7 +38,7 @@ Class BiPositive (PROP : bi) :=
   bi_positive (P Q : PROP) : <affine> (P ∗ Q) ⊢ <affine> P ∗ Q.
 Global Hint Mode BiPositive ! : typeclass_instances.
 
-Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := (True ∗ P)%I.
+Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := True ∗ P.
 Global Arguments bi_absorbingly {_} _%I : simpl never.
 Global Instance: Params (@bi_absorbingly) 1 := {}.
 Typeclasses Opaque bi_absorbingly.
@@ -88,13 +88,13 @@ Fixpoint bi_laterN {PROP : bi} (n : nat) (P : PROP) : PROP :=
   match n with
   | O => P
   | S n' => â–· â–·^n' P
-  end%I
+  end
 where "â–·^ n P" := (bi_laterN n P) : bi_scope.
 Global Arguments bi_laterN {_} !_%nat_scope _%I.
 Global Instance: Params (@bi_laterN) 2 := {}.
 Notation "â–·? p P" := (bi_laterN (Nat.b2n p) P) : bi_scope.
 
-Definition bi_except_0 {PROP : bi} (P : PROP) : PROP := (▷ False ∨ P)%I.
+Definition bi_except_0 {PROP : bi} (P : PROP) : PROP := ▷ False ∨ P.
 Global Arguments bi_except_0 {_} _%I : simpl never.
 Notation "â—‡ P" := (bi_except_0 P) : bi_scope.
 Global Instance: Params (@bi_except_0) 1 := {}.
@@ -112,7 +112,7 @@ Global Instance: Params (@Timeless) 1 := {}.
 Definition bi_wandM {PROP : bi} (mP : option PROP) (Q : PROP) : PROP :=
   match mP with
   | None => Q
-  | Some P => (P -∗ Q)%I
+  | Some P => P -∗ Q
   end.
 Global Arguments bi_wandM {_} !_%I _%I /.
 Notation "mP -∗? Q" := (bi_wandM mP Q)
diff --git a/iris/bi/derived_laws.v b/iris/bi/derived_laws.v
index 53e98c724..b7bc9d5a9 100644
--- a/iris/bi/derived_laws.v
+++ b/iris/bi/derived_laws.v
@@ -607,7 +607,7 @@ Lemma pure_wand_forall φ P `{!Absorbing P} : (⌜φ⌝ -∗ P) ⊣⊢ (∀ _ :
 Proof.
   apply (anti_symm _).
   - apply forall_intro=> Hφ.
-    rewrite -(pure_intro φ emp%I) // emp_wand //.
+    rewrite -(pure_intro φ emp) // emp_wand //.
   - apply wand_intro_l, wand_elim_l', pure_elim'=> Hφ.
     apply wand_intro_l. rewrite (forall_elim Hφ) comm. by apply absorbing.
 Qed.
@@ -794,7 +794,7 @@ Section bi_affine.
   Context `{BiAffine PROP}.
 
   Global Instance bi_affine_absorbing P : Absorbing P | 0.
-  Proof. by rewrite /Absorbing /bi_absorbingly (affine True%I) left_id. Qed.
+  Proof. by rewrite /Absorbing /bi_absorbingly (affine True) left_id. Qed.
   Global Instance bi_affine_positive : BiPositive PROP.
   Proof. intros P Q. by rewrite !affine_affinely. Qed.
 
@@ -929,7 +929,7 @@ Qed.
 
 Lemma persistently_and_sep_l_1 P Q : <pers> P ∧ Q ⊢ <pers> P ∗ Q.
 Proof.
-  by rewrite -{1}(emp_sep Q%I) persistently_and_sep_assoc and_elim_l.
+  by rewrite -{1}(emp_sep Q) persistently_and_sep_assoc and_elim_l.
 Qed.
 Lemma persistently_and_sep_r_1 P Q : P ∧ <pers> Q ⊢ P ∗ <pers> Q.
 Proof. by rewrite !(comm _ P) persistently_and_sep_l_1. Qed.
@@ -937,7 +937,7 @@ Proof. by rewrite !(comm _ P) persistently_and_sep_l_1. Qed.
 Lemma persistently_and_sep P Q : <pers> (P ∧ Q) ⊢ <pers> (P ∗ Q).
 Proof.
   rewrite persistently_and.
-  rewrite -{1}persistently_idemp -persistently_and -{1}(emp_sep Q%I).
+  rewrite -{1}persistently_idemp -persistently_and -{1}(emp_sep Q).
   by rewrite persistently_and_sep_assoc (comm bi_and) persistently_and_emp_elim.
 Qed.
 
@@ -990,7 +990,7 @@ Proof. intros; rewrite -persistently_and_sep_r_1; auto. Qed.
 Lemma persistently_impl_wand_2 P Q : <pers> (P -∗ Q) ⊢ <pers> (P → Q).
 Proof.
   apply persistently_intro', impl_intro_r.
-  rewrite -{2}(emp_sep P%I) persistently_and_sep_assoc.
+  rewrite -{2}(emp_sep P) persistently_and_sep_assoc.
   by rewrite (comm bi_and) persistently_and_emp_elim wand_elim_l.
 Qed.
 
diff --git a/iris/bi/derived_laws_later.v b/iris/bi/derived_laws_later.v
index 798d76859..70f0dd6b0 100644
--- a/iris/bi/derived_laws_later.v
+++ b/iris/bi/derived_laws_later.v
@@ -111,7 +111,7 @@ Lemma löb `{!BiLöb PROP} P : (▷ P → P) ⊢ P.
 Proof.
   apply entails_impl_True, löb_weak. apply impl_intro_r.
   rewrite -{2}(idemp (∧) (▷ P → P))%I.
-  rewrite {2}(later_intro (▷ P → P))%I.
+  rewrite {2}(later_intro (▷ P → P)).
   rewrite later_impl.
   rewrite assoc impl_elim_l.
   rewrite impl_elim_r. done.
@@ -131,7 +131,7 @@ Proof.
   assert (Q ⊣⊢ (▷ Q → P)) as HQ by (exact: fixpoint_unfold).
   intros HP. rewrite -HP.
   assert (▷ Q ⊢ P) as HQP.
-  { rewrite -HP. rewrite -(idemp (∧) (▷ Q))%I {2}(later_intro (▷ Q))%I.
+  { rewrite -HP. rewrite -(idemp (∧) (▷ Q))%I {2}(later_intro (▷ Q)).
     by rewrite {1}HQ {1}later_impl impl_elim_l. }
   rewrite -HQP HQ -2!later_intro.
   apply (entails_impl_True _ P). done.
@@ -139,15 +139,15 @@ Qed.
 
 Lemma löb_wand_intuitionistically `{!BiLöb PROP} P : □ (□ ▷ P -∗ P) ⊢ P.
 Proof.
-  rewrite -{3}(intuitionistically_elim P) -(löb (□ P)%I). apply impl_intro_l.
+  rewrite -{3}(intuitionistically_elim P) -(löb (□ P)). apply impl_intro_l.
   rewrite {1}intuitionistically_into_persistently_1 later_persistently.
   rewrite persistently_and_intuitionistically_sep_l.
-  rewrite -{1}(intuitionistically_idemp (â–· P)%I) intuitionistically_sep_2.
+  rewrite -{1}(intuitionistically_idemp (â–· P)) intuitionistically_sep_2.
   by rewrite wand_elim_r.
 Qed.
 Lemma löb_wand `{!BiLöb PROP} P : □ (▷ P -∗ P) ⊢ P.
 Proof.
-  by rewrite -(intuitionistically_elim (▷ P)%I) löb_wand_intuitionistically.
+  by rewrite -(intuitionistically_elim (▷ P)) löb_wand_intuitionistically.
 Qed.
 
 (** The proof of the right-to-left direction relies on the BI being affine. It
@@ -322,7 +322,7 @@ Proof. by rewrite {1}(except_0_intro Q) except_0_sep. Qed.
 
 Lemma later_affinely_1 `{!Timeless (PROP:=PROP) emp} P : ▷ <affine> P ⊢ ◇ <affine> ▷ P.
 Proof.
-  rewrite /bi_affinely later_and (timeless emp%I) except_0_and.
+  rewrite /bi_affinely later_and (timeless emp) except_0_and.
   by apply and_mono, except_0_intro.
 Qed.
 
diff --git a/iris/bi/lib/atomic.v b/iris/bi/lib/atomic.v
index c2ea7fc45..d82e531ee 100644
--- a/iris/bi/lib/atomic.v
+++ b/iris/bi/lib/atomic.v
@@ -21,9 +21,8 @@ Section definition.
   (** atomic_acc as the "introduction form" of atomic updates: An accessor
       that can be aborted back to [P]. *)
   Definition atomic_acc Eo Ei α P β Φ : PROP :=
-    (|={Eo, Ei}=> ∃.. x, α x ∗
-          ((α x ={Ei, Eo}=∗ P) ∧ (∀.. y, β x y ={Ei, Eo}=∗ Φ x y))
-    )%I.
+    |={Eo, Ei}=> ∃.. x, α x ∗
+          ((α x ={Ei, Eo}=∗ P) ∧ (∀.. y, β x y ={Ei, Eo}=∗ Φ x y)).
 
   Lemma atomic_acc_wand Eo Ei α P1 P2 β Φ1 Φ2 :
     ((P1 -∗ P2) ∧ (∀.. x y, Φ1 x y -∗ Φ2 x y)) -∗
diff --git a/iris/bi/lib/core.v b/iris/bi/lib/core.v
index fd13d05c1..195de23af 100644
--- a/iris/bi/lib/core.v
+++ b/iris/bi/lib/core.v
@@ -9,7 +9,7 @@ Import bi.
 Definition coreP `{!BiPlainly PROP} (P : PROP) : PROP :=
   (* TODO: Looks like we want notation for affinely-plainly; that lets us avoid
   using conjunction/implication here. *)
-  (∀ Q : PROP, <affine> ■ (Q -∗ <pers> Q) -∗ <affine> ■ (P -∗ Q) -∗ Q)%I.
+  ∀ Q : PROP, <affine> ■ (Q -∗ <pers> Q) -∗ <affine> ■ (P -∗ Q) -∗ Q.
 Global Instance: Params (@coreP) 1 := {}.
 Typeclasses Opaque coreP.
 
diff --git a/iris/bi/lib/counterexamples.v b/iris/bi/lib/counterexamples.v
index 2ddae631c..405653f33 100644
--- a/iris/bi/lib/counterexamples.v
+++ b/iris/bi/lib/counterexamples.v
@@ -42,7 +42,7 @@ Module löb_em. Section löb_em.
 
   Lemma later_anything P : ⊢@{PROP} ▷ P.
   Proof.
-    iDestruct (em (â–· False)%I) as "#[HP|HnotP]".
+    iDestruct (em (â–· False)) as "#[HP|HnotP]".
     - iNext. done.
     - iExFalso. iLöb as "IH". iSpecialize ("HnotP" with "IH"). done.
   Qed.
@@ -81,7 +81,7 @@ Module savedprop. Section savedprop.
   Qed.
 
   (** A bad recursive reference: "Assertion with name [i] does not hold" *)
-  Definition A (i : ident) : PROP := (∃ P, □ ¬ P ∗ saved i P)%I.
+  Definition A (i : ident) : PROP := ∃ P, □ ¬ P ∗ saved i P.
 
   Lemma A_alloc : ⊢ |==> ∃ i, saved i (A i).
   Proof. by apply sprop_alloc_dep. Qed.
@@ -120,7 +120,6 @@ Module inv. Section inv.
   (** We have the update modality (two classes: empty/full mask) *)
   Inductive mask := M0 | M1.
   Context (fupd : mask → PROP → PROP).
-  Global Arguments fupd _ _%I.
   Hypothesis fupd_intro : ∀ E P, P ⊢ fupd E P.
   Hypothesis fupd_mono : ∀ E P Q, (P ⊢ Q) → fupd E P ⊢ fupd E Q.
   Hypothesis fupd_fupd : ∀ E P, fupd E (fupd E P) ⊢ fupd E P.
@@ -198,13 +197,13 @@ Module inv. Section inv.
 
   (** Now to the actual counterexample. We start with a weird form of saved propositions. *)
   Definition saved (γ : gname) (P : PROP) : PROP :=
-    (∃ i, inv i (start γ ∨ (finished γ ∗ □ P)))%I.
+    ∃ i, inv i (start γ ∨ (finished γ ∗ □ P)).
   Global Instance saved_persistent γ P : Persistent (saved γ P) := _.
 
   Lemma saved_alloc (P : gname → PROP) : ⊢ fupd M1 (∃ γ, saved γ (P γ)).
   Proof.
     iIntros "". iMod (sts_alloc) as (γ) "Hs".
-    iMod (inv_alloc (start γ ∨ (finished γ ∗ □ (P γ)))%I with "[Hs]") as (i) "#Hi".
+    iMod (inv_alloc (start γ ∨ (finished γ ∗ □ (P γ))) with "[Hs]") as (i) "#Hi".
     { auto. }
     iApply fupd_intro. by iExists γ, i.
   Qed.
@@ -231,7 +230,7 @@ Module inv. Section inv.
 
   (** And now we tie a bad knot. *)
   Notation not_fupd P := (□ (P -∗ fupd M1 False))%I.
-  Definition A i : PROP := (∃ P, not_fupd P ∗ saved i P)%I.
+  Definition A i : PROP := ∃ P, not_fupd P ∗ saved i P.
   Global Instance A_persistent i : Persistent (A i) := _.
 
   Lemma A_alloc : ⊢ fupd M1 (∃ i, saved i (A i)).
@@ -287,7 +286,6 @@ Module linear. Section linear.
   (** We have the mask-changing update modality (two classes: empty/full mask) *)
   Inductive mask := M0 | M1.
   Context (fupd : mask → mask → PROP → PROP).
-  Global Arguments fupd _ _ _%I.
   Hypothesis fupd_intro : ∀ E P, P ⊢ fupd E E P.
   Hypothesis fupd_mono : ∀ E1 E2 P Q, (P ⊢ Q) → fupd E1 E2 P ⊢ fupd E1 E2 Q.
   Hypothesis fupd_fupd : ∀ E1 E2 E3 P, fupd E1 E2 (fupd E2 E3 P) ⊢ fupd E1 E3 P.
@@ -324,7 +322,7 @@ Module linear. Section linear.
   Lemma leak P : P -∗ fupd M1 M1 emp.
   Proof.
     iIntros "HP".
-    iMod ((cinv_alloc _ True%I) with "[//]") as (γ) "[Hinv Htok]".
+    iMod (cinv_alloc _ True with "[//]") as (γ) "[Hinv Htok]".
     iMod (cinv_acc with "Hinv Htok") as "(Htrue & Htok & Hclose)".
     iApply "Hclose". done.
   Qed.
diff --git a/iris/bi/lib/laterable.v b/iris/bi/lib/laterable.v
index 0ab92ec48..92fa67708 100644
--- a/iris/bi/lib/laterable.v
+++ b/iris/bi/lib/laterable.v
@@ -71,7 +71,7 @@ Section instances.
 
   (* A wrapper to obtain a weaker, laterable form of any assertion. *)
   Definition make_laterable (Q : PROP) : PROP :=
-    (∃ P, ▷ P ∗ □ (▷ P -∗ Q))%I.
+    ∃ P, ▷ P ∗ □ (▷ P -∗ Q).
 
   Global Instance make_laterable_ne : NonExpansive make_laterable.
   Proof. solve_proper. Qed.
diff --git a/iris/bi/lib/relations.v b/iris/bi/lib/relations.v
index 04a640392..9d7a37635 100644
--- a/iris/bi/lib/relations.v
+++ b/iris/bi/lib/relations.v
@@ -10,7 +10,7 @@ Set Default Proof Using "Type*".
 Definition bi_rtc_pre `{!BiInternalEq PROP}
     {A : ofe} (R : A → A → PROP)
     (x2 : A) (rec : A → PROP) (x1 : A) : PROP :=
-  (<affine> (x1 ≡ x2) ∨ ∃ x', R x1 x' ∗ rec x')%I.
+  <affine> (x1 ≡ x2) ∨ ∃ x', R x1 x' ∗ rec x'.
 
 Global Instance bi_rtc_pre_mono `{!BiInternalEq PROP}
     {A : ofe} (R : A → A → PROP) `{NonExpansive2 R} (x : A) :
diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index 3c31215a9..30f159eb8 100644
--- a/iris/bi/monpred.v
+++ b/iris/bi/monpred.v
@@ -743,19 +743,19 @@ Lemma monPred_objectively_big_sepMS `{BiIndexBottom bot} `{Countable A}
 Proof. apply (big_opMS_commute _). Qed.
 
 Global Instance big_sepL_objective {A} (l : list A) Φ `{∀ n x, Objective (Φ n x)} :
-  @Objective I PROP ([∗ list] n↦x ∈ l, Φ n x)%I.
+  @Objective I PROP ([∗ list] n↦x ∈ l, Φ n x).
 Proof. generalize dependent Φ. induction l=>/=; apply _. Qed.
 Global Instance big_sepM_objective `{Countable K} {A}
        (Φ : K → A → monPred) (m : gmap K A) `{∀ k x, Objective (Φ k x)} :
-  Objective ([∗ map] k↦x ∈ m, Φ k x)%I.
+  Objective ([∗ map] k↦x ∈ m, Φ k x).
 Proof. intros ??. rewrite !monPred_at_big_sepM. do 3 f_equiv. by apply objective_at. Qed.
 Global Instance big_sepS_objective `{Countable A} (Φ : A → monPred)
        (X : gset A) `{∀ y, Objective (Φ y)} :
-  Objective ([∗ set] y ∈ X, Φ y)%I.
+  Objective ([∗ set] y ∈ X, Φ y).
 Proof. intros ??. rewrite !monPred_at_big_sepS. do 2 f_equiv. by apply objective_at. Qed.
 Global Instance big_sepMS_objective `{Countable A} (Φ : A → monPred)
        (X : gmultiset A) `{∀ y, Objective (Φ y)} :
-  Objective ([∗ mset] y ∈ X, Φ y)%I.
+  Objective ([∗ mset] y ∈ X, Φ y).
 Proof. intros ??. rewrite !monPred_at_big_sepMS. do 2 f_equiv. by apply objective_at. Qed.
 
 (** BUpd *)
@@ -784,7 +784,7 @@ Lemma monPred_at_bupd `{BiBUpd PROP} i P : (|==> P) i ⊣⊢ |==> P i.
 Proof. by rewrite monPred_bupd_eq. Qed.
 
 Global Instance bupd_objective `{BiBUpd PROP} P `{!Objective P} :
-  Objective (|==> P)%I.
+  Objective (|==> P).
 Proof. intros ??. by rewrite !monPred_at_bupd objective_at. Qed.
 
 Global Instance monPred_bi_embed_bupd `{BiBUpd PROP} :
@@ -915,7 +915,7 @@ Lemma monPred_at_fupd `{BiFUpd PROP} i E1 E2 P :
 Proof. by rewrite monPred_fupd_eq. Qed.
 
 Global Instance fupd_objective E1 E2 P `{!Objective P} `{BiFUpd PROP} :
-  Objective (|={E1,E2}=> P)%I.
+  Objective (|={E1,E2}=> P).
 Proof. intros ??. by rewrite !monPred_at_fupd objective_at. Qed.
 
 (** Plainly *)
diff --git a/iris/bi/plainly.v b/iris/bi/plainly.v
index 2a016fb62..dff0afd99 100644
--- a/iris/bi/plainly.v
+++ b/iris/bi/plainly.v
@@ -138,7 +138,7 @@ Proof. destruct p; last done. exact: persistently_elim_plainly. Qed.
 Lemma plainly_persistently_elim P : ■ <pers> P ⊣⊢ ■ P.
 Proof.
   apply (anti_symm _).
-  - rewrite -{1}(left_id True%I bi_and (â–  _)%I) (plainly_emp_intro True%I).
+  - rewrite -{1}(left_id True%I bi_and (â–  _)%I) (plainly_emp_intro True).
     rewrite -{2}(persistently_and_emp_elim P).
     rewrite !and_alt -plainly_forall_2. by apply forall_mono=> -[].
   - by rewrite {1}plainly_idemp_2 (plainly_elim_persistently P).
@@ -208,7 +208,7 @@ Proof.
 Qed.
 
 Lemma plainly_and_sep_l_1 P Q : ■ P ∧ Q ⊢ ■ P ∗ Q.
-Proof. by rewrite -{1}(emp_sep Q%I) plainly_and_sep_assoc and_elim_l. Qed.
+Proof. by rewrite -{1}(emp_sep Q) plainly_and_sep_assoc and_elim_l. Qed.
 Lemma plainly_and_sep_r_1 P Q : P ∧ ■ Q ⊢ P ∗ ■ Q.
 Proof. by rewrite !(comm _ P) plainly_and_sep_l_1. Qed.
 
@@ -217,7 +217,7 @@ Proof. apply (anti_symm _); eauto using plainly_mono, plainly_emp_intro. Qed.
 Lemma plainly_and_sep P Q : ■ (P ∧ Q) ⊢ ■ (P ∗ Q).
 Proof.
   rewrite plainly_and.
-  rewrite -{1}plainly_idemp -plainly_and -{1}(emp_sep Q%I).
+  rewrite -{1}plainly_idemp -plainly_and -{1}(emp_sep Q).
   by rewrite plainly_and_sep_assoc (comm bi_and) plainly_and_emp_elim.
 Qed.
 
@@ -244,7 +244,7 @@ Proof. by rewrite -plainly_and_sep plainly_and -and_sep_plainly. Qed.
 Lemma plainly_sep `{BiPositive PROP} P Q : ■ (P ∗ Q) ⊣⊢ ■ P ∗ ■ Q.
 Proof.
   apply (anti_symm _); auto using plainly_sep_2.
-  rewrite -(plainly_affinely_elim (_ ∗ _)%I) affinely_sep -and_sep_plainly. apply and_intro.
+  rewrite -(plainly_affinely_elim (_ ∗ _)) affinely_sep -and_sep_plainly. apply and_intro.
   - by rewrite (affinely_elim_emp Q) right_id affinely_elim.
   - by rewrite (affinely_elim_emp P) left_id affinely_elim.
 Qed.
@@ -260,7 +260,7 @@ Proof. intros; rewrite -plainly_and_sep_r_1; auto. Qed.
 Lemma plainly_impl_wand_2 P Q : ■ (P -∗ Q) ⊢ ■ (P → Q).
 Proof.
   apply plainly_intro', impl_intro_r.
-  rewrite -{2}(emp_sep P%I) plainly_and_sep_assoc.
+  rewrite -{2}(emp_sep P) plainly_and_sep_assoc.
   by rewrite (comm bi_and) plainly_and_emp_elim wand_elim_l.
 Qed.
 
@@ -579,7 +579,7 @@ Section prop_ext.
     apply (anti_symm (⊢)); last exact: prop_ext_2.
     apply (internal_eq_rewrite' P Q (λ Q, ■ (P ∗-∗ Q))%I);
       [ solve_proper | done | ].
-    rewrite (plainly_emp_intro (P ≡ Q)%I).
+    rewrite (plainly_emp_intro (P ≡ Q)).
     apply plainly_mono, wand_iff_refl.
   Qed.
 
@@ -608,7 +608,7 @@ Section prop_ext.
       by rewrite wand_elim_r.
     - rewrite internal_eq_sym (internal_eq_rewrite _ _
         (λ Q, ■ (True -∗ Q))%I ltac:(shelve)); last solve_proper.
-      by rewrite -entails_wand // -(plainly_emp_intro True%I) True_impl.
+      by rewrite -entails_wand // -(plainly_emp_intro True) True_impl.
   Qed.
 
   (* This proof uses [BiPlainlyExist] and [BiLöb] via [plainly_timeless] and
diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index 47f9ece52..e0f98d618 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -358,7 +358,7 @@ Section fupd_derived.
     rewrite -(fupd_mask_frame E E'); first apply fupd_mono; last done.
     (* The most horrible way to apply fupd_intro_mask *)
     rewrite -[X in (X -∗ _)](right_id emp%I).
-    rewrite (fupd_mask_intro_subseteq (E1 ∖ E2 ∪ E ∖ E1) (E ∖ E2) emp%I); last first.
+    rewrite (fupd_mask_intro_subseteq (E1 ∖ E2 ∪ E ∖ E1) (E ∖ E2) emp); last first.
     { rewrite {1}(union_difference_L _ _ HE). set_solver. }
     rewrite fupd_frame_l fupd_frame_r. apply fupd_elim.
     apply fupd_mono.
@@ -411,7 +411,7 @@ Section fupd_derived.
   Lemma step_fupd_wand Eo Ei P Q : (|={Eo}[Ei]▷=> P) -∗ (P -∗ Q) -∗ |={Eo}[Ei]▷=> Q.
   Proof.
     apply wand_intro_l.
-    by rewrite (later_intro (P -∗ Q)%I) fupd_frame_l -later_sep fupd_frame_l
+    by rewrite (later_intro (P -∗ Q)) fupd_frame_l -later_sep fupd_frame_l
                wand_elim_l.
   Qed.
 
@@ -425,10 +425,10 @@ Section fupd_derived.
     Ei2 ⊆ Ei1 → Eo1 ⊆ Eo2 → (|={Eo1}[Ei1]▷=> P) ⊢ |={Eo2}[Ei2]▷=> P.
   Proof.
     intros ??. rewrite -(emp_sep (|={Eo1}[Ei1]â–·=> P)%I).
-    rewrite (fupd_mask_intro_subseteq Eo2 Eo1 emp%I) //.
+    rewrite (fupd_mask_intro_subseteq Eo2 Eo1 emp) //.
     rewrite fupd_frame_r -(fupd_trans Eo2 Eo1 Ei2). f_equiv.
     rewrite fupd_frame_l -(fupd_trans Eo1 Ei1 Ei2). f_equiv.
-    rewrite (fupd_mask_intro_subseteq Ei1 Ei2 (|={_,_}=> emp)%I) //.
+    rewrite (fupd_mask_intro_subseteq Ei1 Ei2 (|={_,_}=> emp)) //.
     rewrite fupd_frame_r. f_equiv.
     rewrite [X in (X ∗ _)%I]later_intro -later_sep. f_equiv.
     rewrite fupd_frame_r -(fupd_trans Ei2 Ei1 Eo2). f_equiv.
@@ -500,7 +500,7 @@ Section fupd_derived.
     Qed.
 
     Lemma fupd_plainly_elim E P : ■ P ={E}=∗ P.
-    Proof. by rewrite (fupd_intro E (â–  P)%I) fupd_plainly_mask. Qed.
+    Proof. by rewrite (fupd_intro E (â–  P)) fupd_plainly_mask. Qed.
 
     Lemma fupd_plainly_keep_r E P R : R ∗ (R ={E}=∗ ■ P) ⊢ |={E}=> R ∗ P.
     Proof. by rewrite !(comm _ R) fupd_plainly_keep_l. Qed.
@@ -543,7 +543,7 @@ Section fupd_derived.
       trans (∀ x, |={E1}=> Φ x)%I.
       { apply forall_mono=> x. by rewrite fupd_plain_mask. }
       rewrite fupd_plain_forall_2. apply fupd_elim.
-      rewrite {1}(plain (∀ x, Φ x)) (fupd_mask_intro_discard E1 E2 (■ _)%I) //.
+      rewrite {1}(plain (∀ x, Φ x)) (fupd_mask_intro_discard E1 E2 (■ _)) //.
       apply fupd_elim. by rewrite fupd_plainly_elim.
     Qed.
     Lemma fupd_plain_forall' E {A} (Φ : A → PROP) `{!∀ x, Plain (Φ x)} :
@@ -552,7 +552,7 @@ Section fupd_derived.
 
     Lemma step_fupd_plain Eo Ei P `{!Plain P} : (|={Eo}[Ei]▷=> P) ={Eo}=∗ ▷ ◇ P.
     Proof.
-      rewrite -(fupd_plain_mask _ Ei (â–· â—‡ P)%I).
+      rewrite -(fupd_plain_mask _ Ei (â–· â—‡ P)).
       apply fupd_elim. by rewrite fupd_plain_mask -fupd_plain_later.
     Qed.
 
diff --git a/iris/program_logic/atomic.v b/iris/program_logic/atomic.v
index 63f075cbc..fead228df 100644
--- a/iris/program_logic/atomic.v
+++ b/iris/program_logic/atomic.v
@@ -15,9 +15,9 @@ Definition atomic_wp `{!irisG Λ Σ} {TA TB : tele}
   (β: TA → TB → iProp Σ) (* atomic post-condition *)
   (f: TA → TB → val Λ) (* Turn the return data into the return value *)
   : iProp Σ :=
-    (∀ (Φ : val Λ → iProp Σ),
-             atomic_update Eo ∅ α β (λ.. x y, Φ (f x y)) -∗
-             WP e {{ Φ }})%I.
+    ∀ (Φ : val Λ → iProp Σ),
+            atomic_update Eo ∅ α β (λ.. x y, Φ (f x y)) -∗
+            WP e {{ Φ }}.
 (* Note: To add a private postcondition, use
    atomic_update α β Eo Ei (λ x y, POST x y -∗ Φ (f x y)) *)
 
diff --git a/iris/program_logic/total_adequacy.v b/iris/program_logic/total_adequacy.v
index 2695ce19c..d1c470c58 100644
--- a/iris/program_logic/total_adequacy.v
+++ b/iris/program_logic/total_adequacy.v
@@ -11,9 +11,9 @@ Implicit Types e : expr Λ.
 
 Definition twptp_pre (twptp : list (expr Λ) → iProp Σ)
     (t1 : list (expr Λ)) : iProp Σ :=
-  (∀ t2 σ1 ns κ κs σ2 nt, ⌜step (t1,σ1) κ (t2,σ2)⌝ -∗
+  ∀ t2 σ1 ns κ κs σ2 nt, ⌜step (t1,σ1) κ (t2,σ2)⌝ -∗
     state_interp σ1 ns κs nt ={⊤}=∗
-              ∃ nt', ⌜κ = []⌝ ∗ state_interp σ2 (S ns) κs nt' ∗ twptp t2)%I.
+              ∃ nt', ⌜κ = []⌝ ∗ state_interp σ2 (S ns) κs nt' ∗ twptp t2.
 
 Lemma twptp_pre_mono (twptp1 twptp2 : list (expr Λ) → iProp Σ) :
   ⊢ <pers> (∀ t, twptp1 t -∗ twptp2 t) →
diff --git a/iris/proofmode/class_instances.v b/iris/proofmode/class_instances.v
index 9b02c4647..b72fc6889 100644
--- a/iris/proofmode/class_instances.v
+++ b/iris/proofmode/class_instances.v
@@ -415,12 +415,12 @@ Global Instance into_wand_affine p q R P Q :
   IntoWand p q R P Q → IntoWand p q (<affine> R) (<affine> P) (<affine> Q).
 Proof.
   rewrite /IntoWand /= => HR. apply wand_intro_r. destruct p; simpl in *.
-  - rewrite (affinely_elim R) -(affine_affinely (â–¡ R)%I) HR. destruct q; simpl in *.
-    + rewrite (affinely_elim P) -{2}(affine_affinely (â–¡ P)%I).
+  - rewrite (affinely_elim R) -(affine_affinely (â–¡ R)) HR. destruct q; simpl in *.
+    + rewrite (affinely_elim P) -{2}(affine_affinely (â–¡ P)).
       by rewrite affinely_sep_2 wand_elim_l.
     + by rewrite affinely_sep_2 wand_elim_l.
   - rewrite HR. destruct q; simpl in *.
-    + rewrite (affinely_elim P) -{2}(affine_affinely (â–¡ P)%I).
+    + rewrite (affinely_elim P) -{2}(affine_affinely (â–¡ P)).
       by rewrite affinely_sep_2 wand_elim_l.
     + by rewrite affinely_sep_2 wand_elim_l.
 Qed.
@@ -437,8 +437,8 @@ Global Instance into_wand_affine_args q R P Q :
   IntoWand true q R P Q → IntoWand' true q R (<affine> P) (<affine> Q).
 Proof.
   rewrite /IntoWand' /IntoWand /= => HR. apply wand_intro_r.
-  rewrite -(affine_affinely (â–¡ R)%I) HR. destruct q; simpl.
-  - rewrite (affinely_elim P) -{2}(affine_affinely (â–¡ P)%I).
+  rewrite -(affine_affinely (â–¡ R)) HR. destruct q; simpl.
+  - rewrite (affinely_elim P) -{2}(affine_affinely (â–¡ P)).
     by rewrite affinely_sep_2 wand_elim_l.
   - by rewrite affinely_sep_2 wand_elim_l.
 Qed.
@@ -645,7 +645,7 @@ Proof. by rewrite /IntoSep. Qed.
 
 Inductive AndIntoSep : PROP → PROP → PROP → PROP → Prop :=
   | and_into_sep_affine P Q Q' : Affine P → FromAffinely Q' Q → AndIntoSep P P Q Q'
-  | and_into_sep P Q : AndIntoSep P (<affine> P)%I Q Q.
+  | and_into_sep P Q : AndIntoSep P (<affine> P) Q Q.
 Existing Class AndIntoSep.
 Global Existing Instance and_into_sep_affine | 0.
 Global Existing Instance and_into_sep | 2.
@@ -873,7 +873,7 @@ Global Instance into_forall_wand_pure a φ P Q :
 Proof.
   rewrite /FromPureT /FromPure /IntoForall=> -[φ' [-> <-]] /=.
   apply forall_intro=>? /=. rewrite -affinely_affinely_if.
-  by rewrite -(pure_intro _ True%I) // /bi_affinely right_id emp_wand.
+  by rewrite -(pure_intro _ True) // /bi_affinely right_id emp_wand.
 Qed.
 
 (* These instances must be used only after [into_forall_wand_pure] and
diff --git a/iris/proofmode/class_instances_embedding.v b/iris/proofmode/class_instances_embedding.v
index 2cbcaf760..44a3e0645 100644
--- a/iris/proofmode/class_instances_embedding.v
+++ b/iris/proofmode/class_instances_embedding.v
@@ -67,9 +67,9 @@ Global Instance into_wand_affine_embed_true q P Q R :
   IntoWand true q R P Q → IntoWand true q ⎡R⎤ (<affine> ⎡P⎤) (<affine> ⎡Q⎤) | 100.
 Proof.
   rewrite /IntoWand /=.
-  rewrite -(intuitionistically_idemp ⎡ _ ⎤%I) embed_intuitionistically_2=> ->.
+  rewrite -(intuitionistically_idemp ⎡ _ ⎤) embed_intuitionistically_2=> ->.
   apply bi.wand_intro_l. destruct q; simpl.
-  - rewrite affinely_elim  -(intuitionistically_idemp ⎡ _ ⎤%I).
+  - rewrite affinely_elim  -(intuitionistically_idemp ⎡ _ ⎤).
     rewrite embed_intuitionistically_2 intuitionistically_sep_2 -embed_sep.
     by rewrite wand_elim_r intuitionistically_affinely.
   - by rewrite intuitionistically_affinely affinely_sep_2 -embed_sep wand_elim_r.
diff --git a/iris/proofmode/class_instances_later.v b/iris/proofmode/class_instances_later.v
index d4c7e2d3a..87d1c84a4 100644
--- a/iris/proofmode/class_instances_later.v
+++ b/iris/proofmode/class_instances_later.v
@@ -10,13 +10,13 @@ Implicit Types P Q R : PROP.
 
 (** FromAssumption *)
 Global Instance from_assumption_later p P Q :
-  FromAssumption p P Q → KnownRFromAssumption p P (▷ Q)%I.
+  FromAssumption p P Q → KnownRFromAssumption p P (▷ Q).
 Proof. rewrite /KnownRFromAssumption /FromAssumption=>->. apply later_intro. Qed.
 Global Instance from_assumption_laterN n p P Q :
-  FromAssumption p P Q → KnownRFromAssumption p P (▷^n Q)%I.
+  FromAssumption p P Q → KnownRFromAssumption p P (▷^n Q).
 Proof. rewrite /KnownRFromAssumption /FromAssumption=>->. apply laterN_intro. Qed.
 Global Instance from_assumption_except_0 p P Q :
-  FromAssumption p P Q → KnownRFromAssumption p P (◇ Q)%I.
+  FromAssumption p P Q → KnownRFromAssumption p P (◇ Q).
 Proof. rewrite /KnownRFromAssumption /FromAssumption=>->. apply except_0_intro. Qed.
 
 (** FromPure *)
@@ -39,7 +39,7 @@ Global Instance into_wand_later_args p q R P Q :
 Proof.
   rewrite /IntoWand' /IntoWand /= => HR.
   by rewrite !later_intuitionistically_if_2
-             (later_intro (â–¡?p R)%I) -later_wand HR.
+             (later_intro (â–¡?p R)) -later_wand HR.
 Qed.
 Global Instance into_wand_laterN n p q R P Q :
   IntoWand p q R P Q → IntoWand p q (▷^n R) (▷^n P) (▷^n Q).
@@ -52,7 +52,7 @@ Global Instance into_wand_laterN_args n p q R P Q :
 Proof.
   rewrite /IntoWand' /IntoWand /= => HR.
   by rewrite !laterN_intuitionistically_if_2
-             (laterN_intro _ (â–¡?p R)%I) -laterN_wand HR.
+             (laterN_intro _ (â–¡?p R)) -laterN_wand HR.
 Qed.
 
 (** FromAnd *)
@@ -186,15 +186,15 @@ Proof. rewrite /IntoForall=> HP. by rewrite HP except_0_forall. Qed.
 
 (** FromForall *)
 Global Instance from_forall_later {A} P (Φ : A → PROP) name :
-  FromForall P Φ name → FromForall (▷ P)%I (λ a, ▷ (Φ a))%I name.
+  FromForall P Φ name → FromForall (▷ P) (λ a, ▷ (Φ a))%I name.
 Proof. rewrite /FromForall=> <-. by rewrite later_forall. Qed.
 
 Global Instance from_forall_laterN {A} P (Φ : A → PROP) n name :
-      FromForall P Φ name → FromForall (▷^n P)%I (λ a, ▷^n (Φ a))%I name.
+      FromForall P Φ name → FromForall (▷^n P) (λ a, ▷^n (Φ a))%I name.
 Proof. rewrite /FromForall => <-. by rewrite laterN_forall. Qed.
 
 Global Instance from_forall_except_0 {A} P (Φ : A → PROP) name :
-  FromForall P Φ name → FromForall (◇ P)%I (λ a, ◇ (Φ a))%I name.
+  FromForall P Φ name → FromForall (◇ P) (λ a, ◇ (Φ a))%I name.
 Proof. rewrite /FromForall=> <-. by rewrite except_0_forall. Qed.
 
 (** IsExcept0 *)
@@ -238,7 +238,7 @@ Proof. rewrite /IntoExcept0=> ->. by rewrite except_0_persistently. Qed.
 Global Instance elim_modal_timeless p P P' Q :
   IntoExcept0 P P' → IsExcept0 Q → ElimModal True p p P P' Q Q.
 Proof.
-  intros. rewrite /ElimModal (except_0_intro (_ -∗ _)%I) (into_except_0 P).
+  intros. rewrite /ElimModal (except_0_intro (_ -∗ _)) (into_except_0 P).
   by rewrite except_0_intuitionistically_if_2 -except_0_sep wand_elim_r.
 Qed.
 
@@ -247,23 +247,23 @@ Qed.
 Global Instance add_modal_later_except_0 P Q :
   Timeless P → AddModal (▷ P) P (◇ Q) | 0.
 Proof.
-  intros. rewrite /AddModal (except_0_intro (_ -∗ _)%I) (timeless P).
+  intros. rewrite /AddModal (except_0_intro (_ -∗ _)) (timeless P).
   by rewrite -except_0_sep wand_elim_r except_0_idemp.
 Qed.
 Global Instance add_modal_later P Q :
   Timeless P → AddModal (▷ P) P (▷ Q) | 0.
 Proof.
-  intros. rewrite /AddModal (except_0_intro (_ -∗ _)%I) (timeless P).
+  intros. rewrite /AddModal (except_0_intro (_ -∗ _)) (timeless P).
   by rewrite -except_0_sep wand_elim_r except_0_later.
 Qed.
 Global Instance add_modal_except_0 P Q : AddModal (â—‡ P) P (â—‡ Q) | 1.
 Proof.
-  intros. rewrite /AddModal (except_0_intro (_ -∗ _)%I).
+  intros. rewrite /AddModal (except_0_intro (_ -∗ _)).
   by rewrite -except_0_sep wand_elim_r except_0_idemp.
 Qed.
 Global Instance add_modal_except_0_later P Q : AddModal (â—‡ P) P (â–· Q) | 1.
 Proof.
-  intros. rewrite /AddModal (except_0_intro (_ -∗ _)%I).
+  intros. rewrite /AddModal (except_0_intro (_ -∗ _)).
   by rewrite -except_0_sep wand_elim_r except_0_later.
 Qed.
 
diff --git a/iris/proofmode/class_instances_plainly.v b/iris/proofmode/class_instances_plainly.v
index b49f42a76..44353c915 100644
--- a/iris/proofmode/class_instances_plainly.v
+++ b/iris/proofmode/class_instances_plainly.v
@@ -84,7 +84,7 @@ Global Instance into_forall_plainly {A} P (Φ : A → PROP) :
 Proof. rewrite /IntoForall=> HP. by rewrite HP plainly_forall. Qed.
 
 Global Instance from_forall_plainly {A} P (Φ : A → PROP) name :
-  FromForall P Φ name → FromForall (■ P)%I (λ a, ■ (Φ a))%I name.
+  FromForall P Φ name → FromForall (■ P) (λ a, ■ (Φ a))%I name.
 Proof. rewrite /FromForall=> <-. by rewrite plainly_forall. Qed.
 
 Global Instance from_modal_plainly P :
diff --git a/iris/proofmode/class_instances_updates.v b/iris/proofmode/class_instances_updates.v
index 5fd7fea8b..b0ab10ecc 100644
--- a/iris/proofmode/class_instances_updates.v
+++ b/iris/proofmode/class_instances_updates.v
@@ -14,7 +14,7 @@ Global Instance from_assumption_bupd `{!BiBUpd PROP} p P Q :
 Proof. rewrite /KnownRFromAssumption /FromAssumption=>->. apply bupd_intro. Qed.
 Global Instance from_assumption_fupd
     `{!BiBUpd PROP, !BiFUpd PROP, !BiBUpdFUpd PROP} E p P Q :
-  FromAssumption p P (|==> Q) → KnownRFromAssumption p P (|={E}=> Q)%I.
+  FromAssumption p P (|==> Q) → KnownRFromAssumption p P (|={E}=> Q).
 Proof. rewrite /KnownRFromAssumption /FromAssumption=>->. apply bupd_fupd. Qed.
 
 Global Instance from_pure_bupd `{!BiBUpd PROP} a P φ :
@@ -100,7 +100,7 @@ Global Instance from_forall_fupd
   (* Some cases in which [E2 ⊆ E1] holds *)
   TCOr (TCEq E1 E2) (TCOr (TCEq E1 ⊤) (TCEq E2 ∅)) →
   FromForall P Φ name → (∀ x, Plain (Φ x)) →
-  FromForall (|={E1,E2}=> P)%I (λ a, |={E1,E2}=> (Φ a))%I name.
+  FromForall (|={E1,E2}=> P) (λ a, |={E1,E2}=> (Φ a))%I name.
 Proof.
   rewrite /FromForall=> -[->|[->|->]] <- ?; rewrite fupd_plain_forall; set_solver.
 Qed.
@@ -109,7 +109,7 @@ Global Instance from_forall_step_fupd
   (* Some cases in which [E2 ⊆ E1] holds *)
   TCOr (TCEq E1 E2) (TCOr (TCEq E1 ⊤) (TCEq E2 ∅)) →
   FromForall P Φ name → (∀ x, Plain (Φ x)) →
-  FromForall (|={E1}[E2]▷=> P)%I (λ a, |={E1}[E2]▷=> (Φ a))%I name.
+  FromForall (|={E1}[E2]▷=> P) (λ a, |={E1}[E2]▷=> (Φ a))%I name.
 Proof.
   rewrite /FromForall=> -[->|[->|->]] <- ?; rewrite step_fupd_plain_forall; set_solver.
 Qed.
diff --git a/iris/proofmode/coq_tactics.v b/iris/proofmode/coq_tactics.v
index 0451e6559..617d76f43 100644
--- a/iris/proofmode/coq_tactics.v
+++ b/iris/proofmode/coq_tactics.v
@@ -26,7 +26,7 @@ Lemma tac_stop Δ P :
    | Enil, Γs => env_to_prop Γs
    | Γp, Enil => □ env_to_prop_and Γp
    | Γp, Γs => □ env_to_prop_and Γp ∗ env_to_prop Γs
-   end%I ⊢ P) →
+   end ⊢ P) →
   envs_entails Δ P.
 Proof.
   rewrite envs_entails_eq !of_envs_eq. intros <-.
@@ -166,7 +166,7 @@ Proof.
   - destruct HPQ.
     + rewrite -(affine_affinely P) (into_pure P) -persistent_and_affinely_sep_l.
       by apply pure_elim_l.
-    + rewrite (into_pure P) -(persistent_absorbingly_affinely ⌜ _ ⌝%I) absorbingly_sep_lr.
+    + rewrite (into_pure P) -(persistent_absorbingly_affinely ⌜ _ ⌝) absorbingly_sep_lr.
       rewrite -persistent_and_affinely_sep_l. apply pure_elim_l=> ?. by rewrite HQ.
 Qed.
 
@@ -462,10 +462,10 @@ Class IntoIH (φ : Prop) (Δ : envs PROP) (Q : PROP) :=
 Global Instance into_ih_entails Δ Q : IntoIH (envs_entails Δ Q) Δ Q.
 Proof. by rewrite envs_entails_eq /IntoIH. Qed.
 Global Instance into_ih_forall {A} (φ : A → Prop) Δ Φ :
-  (∀ x, IntoIH (φ x) Δ (Φ x)) → IntoIH (∀ x, φ x) Δ (∀ x, Φ x)%I | 2.
+  (∀ x, IntoIH (φ x) Δ (Φ x)) → IntoIH (∀ x, φ x) Δ (∀ x, Φ x) | 2.
 Proof. rewrite /IntoIH=> HΔ ?. apply forall_intro=> x. by rewrite (HΔ x). Qed.
 Global Instance into_ih_impl (φ ψ : Prop) Δ Q :
-  IntoIH φ Δ Q → IntoIH (ψ → φ) Δ (⌜ψ⌝ → Q)%I | 1.
+  IntoIH φ Δ Q → IntoIH (ψ → φ) Δ (⌜ψ⌝ → Q) | 1.
 Proof. rewrite /IntoIH=> HΔ ?. apply impl_intro_l, pure_elim_l. auto. Qed.
 
 Lemma tac_revert_ih Δ P Q {φ : Prop} (Hφ : φ) :
@@ -828,7 +828,7 @@ Proof.
   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) //=.
-  rewrite HP HPxy (intuitionistically_if_elim _ (_ ≡ _)%I) sep_elim_l.
+  rewrite HP HPxy (intuitionistically_if_elim _ (_ ≡ _)) sep_elim_l.
   rewrite persistent_and_affinely_sep_r -assoc. apply wand_elim_r'.
   rewrite -persistent_and_affinely_sep_r. apply impl_elim_r'. destruct d.
   - apply (internal_eq_rewrite x y (λ y, □?q Φ y -∗ of_envs Δ')%I). solve_proper.
@@ -1023,7 +1023,7 @@ Section tac_modal_intro.
     - intros ?. rewrite HΓ //. destruct Hif as [-> [? ->| ->]| ->].
       + by rewrite (affine P) left_id.
       + by rewrite right_id comm (True_intro P).
-      + by rewrite comm -assoc (True_intro (_ ∗ P)%I).
+      + by rewrite comm -assoc (True_intro (_ ∗ P)).
     - inversion 1; auto.
     - intros j. destruct (ident_beq _ _); naive_solver.
   Qed.
@@ -1071,8 +1071,8 @@ Section tac_modal_intro.
         rewrite -(right_id emp%I bi_sep (M _)).
         eauto using modality_spatial_transform.
     - rewrite -HQ' /= right_id comm -{2}(modality_spatial_clear M) //.
-      by rewrite (True_intro ([∗] Γs)%I).
-    - rewrite -HQ' {1}(modality_spatial_id M ([∗] Γs)%I) //.
+      by rewrite (True_intro ([∗] Γs)).
+    - rewrite -HQ' {1}(modality_spatial_id M ([∗] Γs)) //.
       by rewrite -modality_sep.
   Qed.
 End tac_modal_intro.
diff --git a/iris/proofmode/frame_instances.v b/iris/proofmode/frame_instances.v
index 9b7fba1f7..178576f4d 100644
--- a/iris/proofmode/frame_instances.v
+++ b/iris/proofmode/frame_instances.v
@@ -210,7 +210,7 @@ Global Instance frame_affinely p R P Q Q' :
   Frame p R P Q → MakeAffinely Q Q' → Frame p R (<affine> P) Q'.
 Proof.
   rewrite /Frame /MakeAffinely=> -[->|?] <- <- /=;
-    by rewrite -{1}(affine_affinely (_ R)%I) affinely_sep_2.
+    by rewrite -{1}(affine_affinely (_ R)) affinely_sep_2.
 Qed.
 
 Global Instance make_intuitionistically_emp :
@@ -347,6 +347,6 @@ Global Instance frame_except_0 p R P Q Q' :
   Frame p R P Q → MakeExcept0 Q Q' → Frame p R (◇ P) Q'.
 Proof.
   rewrite /Frame /MakeExcept0=><- <-.
-  by rewrite except_0_sep -(except_0_intro (â–¡?p R)%I).
+  by rewrite except_0_sep -(except_0_intro (â–¡?p R)).
 Qed.
 End bi.
diff --git a/iris/proofmode/monpred.v b/iris/proofmode/monpred.v
index bd70d2493..0a7db19c0 100644
--- a/iris/proofmode/monpred.v
+++ b/iris/proofmode/monpred.v
@@ -142,7 +142,7 @@ Proof. by rewrite /MakeMonPredAt monPred_at_in. Qed.
 Global Instance make_monPred_at_default i P : MakeMonPredAt i P (P i) | 100.
 Proof. by rewrite /MakeMonPredAt. Qed.
 Global Instance make_monPred_at_bupd `{BiBUpd PROP} i P 𝓟 :
-  MakeMonPredAt i P 𝓟 → MakeMonPredAt i (|==> P)%I (|==> 𝓟)%I.
+  MakeMonPredAt i P 𝓟 → MakeMonPredAt i (|==> P) (|==> 𝓟).
 Proof. by rewrite /MakeMonPredAt monPred_at_bupd=> <-. Qed.
 
 Global Instance from_assumption_make_monPred_at_l p i j P 𝓟 :
@@ -480,16 +480,16 @@ Global Instance make_monPred_at_internal_eq `{!BiInternalEq PROP} {A : ofe} (x y
   MakeMonPredAt i (x ≡ y) (x ≡ y).
 Proof. by rewrite /MakeMonPredAt monPred_at_internal_eq. Qed.
 Global Instance make_monPred_at_except_0 i P 𝓠 :
-  MakeMonPredAt i P 𝓠 → MakeMonPredAt i (◇ P)%I (◇ 𝓠)%I.
+  MakeMonPredAt i P 𝓠 → MakeMonPredAt i (◇ P) (◇ 𝓠).
 Proof. by rewrite /MakeMonPredAt monPred_at_except_0=><-. Qed.
 Global Instance make_monPred_at_later i P 𝓠 :
-  MakeMonPredAt i P 𝓠 → MakeMonPredAt i (▷ P)%I (▷ 𝓠)%I.
+  MakeMonPredAt i P 𝓠 → MakeMonPredAt i (▷ P) (▷ 𝓠).
 Proof. by rewrite /MakeMonPredAt monPred_at_later=><-. Qed.
 Global Instance make_monPred_at_laterN i n P 𝓠 :
-  MakeMonPredAt i P 𝓠 → MakeMonPredAt i (▷^n P)%I (▷^n 𝓠)%I.
+  MakeMonPredAt i P 𝓠 → MakeMonPredAt i (▷^n P) (▷^n 𝓠).
 Proof. rewrite /MakeMonPredAt=> <-. elim n=>//= ? <-. by rewrite monPred_at_later. Qed.
 Global Instance make_monPred_at_fupd `{BiFUpd PROP} i E1 E2 P 𝓟 :
-  MakeMonPredAt i P 𝓟 → MakeMonPredAt i (|={E1,E2}=> P)%I (|={E1,E2}=> 𝓟)%I.
+  MakeMonPredAt i P 𝓟 → MakeMonPredAt i (|={E1,E2}=> P) (|={E1,E2}=> 𝓟).
 Proof. by rewrite /MakeMonPredAt monPred_at_fupd=> <-. Qed.
 
 Global Instance into_internal_eq_monPred_at `{!BiInternalEq PROP}
-- 
GitLab