diff --git a/_CoqProject b/_CoqProject
index 78107d894c1259c79f5cb919085e29eaa72bb2e4..c0f4282236a02e76fd9f8e8c9c46ae804b0a6f7f 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -19,8 +19,6 @@
 -arg -w -arg -redundant-canonical-projection
 # Some warnings exist only on some Coq versions
 -arg -w -arg -unknown-warning
-# Fixing this one requires Coq 8.19
--arg -w -arg -argument-scope-delimiter
 # https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
 -arg -w -arg -notation-incompatible-prefix
 
diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 318577d095d5bfa1a2bf89b93c664485b89d54ba..b47f5368177b4433fe71cd29966ec2624b76ea6b 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -1852,7 +1852,7 @@ Section sigTOF.
     repeat intro. apply sigT_map => a. exact: oFunctor_map_contractive.
   Qed.
 End sigTOF.
-Global Arguments sigTOF {_} _%OF.
+Global Arguments sigTOF {_} _%_OF.
 
 Notation "{ x  &  P }" := (sigTOF (λ x, P%OF)) : oFunctor_scope.
 Notation "{ x : A &  P }" := (@sigTOF A%type (λ x, P%OF)) : oFunctor_scope.
diff --git a/iris/bi/derived_connectives.v b/iris/bi/derived_connectives.v
index a867721761d40b5bad201d57b4440ae28604927b..3af9d2e96456e3bfa106180d367117849c22e266 100644
--- a/iris/bi/derived_connectives.v
+++ b/iris/bi/derived_connectives.v
@@ -3,82 +3,82 @@ 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).
-Global Arguments bi_iff {_} _%I _%I : simpl never.
+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).
-Global Arguments bi_wand_iff {_} _%I _%I : simpl never.
+Global Arguments bi_wand_iff {_} _%_I _%_I : simpl never.
 Global Instance: Params (@bi_wand_iff) 1 := {}.
 Infix "∗-∗" := bi_wand_iff : bi_scope.
 Notation "P ∗-∗ Q" := (⊢ P ∗-∗ Q) : stdpp_scope.
 
 Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ <pers> P.
-Global Arguments Persistent {_} _%I : simpl never.
-Global Arguments persistent {_} _%I {_}.
+Global Arguments Persistent {_} _%_I : simpl never.
+Global Arguments persistent {_} _%_I {_}.
 Global Hint Mode Persistent + ! : typeclass_instances.
 Global Instance: Params (@Persistent) 1 := {}.
 Global Hint Extern 100 (Persistent (match ?x with _ => _ end)) =>
   destruct x : typeclass_instances.
 
 Definition bi_affinely {PROP : bi} (P : PROP) : PROP := emp ∧ P.
-Global Arguments bi_affinely {_} _%I : simpl never.
+Global Arguments bi_affinely {_} _%_I : simpl never.
 Global Instance: Params (@bi_affinely) 1 := {}.
 Global Typeclasses Opaque bi_affinely.
 Notation "'<affine>' P" := (bi_affinely P) : bi_scope.
 
 Class Affine {PROP : bi} (Q : PROP) := affine : Q ⊢ emp.
-Global Arguments Affine {_} _%I : simpl never.
-Global Arguments affine {_} _%I {_}.
+Global Arguments Affine {_} _%_I : simpl never.
+Global Arguments affine {_} _%_I {_}.
 Global Hint Mode Affine + ! : typeclass_instances.
 Global Hint Extern 100 (Affine (match ?x with _ => _ end)) =>
   destruct x : typeclass_instances.
 
 Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := True ∗ P.
-Global Arguments bi_absorbingly {_} _%I : simpl never.
+Global Arguments bi_absorbingly {_} _%_I : simpl never.
 Global Instance: Params (@bi_absorbingly) 1 := {}.
 Global Typeclasses Opaque bi_absorbingly.
 Notation "'<absorb>' P" := (bi_absorbingly P) : bi_scope.
 
 Class Absorbing {PROP : bi} (P : PROP) := absorbing : <absorb> P ⊢ P.
-Global Arguments Absorbing {_} _%I : simpl never.
-Global Arguments absorbing {_} _%I.
+Global Arguments Absorbing {_} _%_I : simpl never.
+Global Arguments absorbing {_} _%_I.
 Global Hint Mode Absorbing + ! : typeclass_instances.
 Global Hint Extern 100 (Absorbing (match ?x with _ => _ end)) =>
   destruct x : typeclass_instances.
 
 Definition bi_persistently_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
   (if p then <pers> P else P)%I.
-Global Arguments bi_persistently_if {_} !_ _%I /.
+Global Arguments bi_persistently_if {_} !_ _%_I /.
 Global Instance: Params (@bi_persistently_if) 2 := {}.
 Global Typeclasses Opaque bi_persistently_if.
 Notation "'<pers>?' p P" := (bi_persistently_if p P) : bi_scope.
 
 Definition bi_affinely_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
   (if p then <affine> P else P)%I.
-Global Arguments bi_affinely_if {_} !_ _%I /.
+Global Arguments bi_affinely_if {_} !_ _%_I /.
 Global Instance: Params (@bi_affinely_if) 2 := {}.
 Global Typeclasses Opaque bi_affinely_if.
 Notation "'<affine>?' p P" := (bi_affinely_if p P) : bi_scope.
 
 Definition bi_absorbingly_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
   (if p then <absorb> P else P)%I.
-Global Arguments bi_absorbingly_if {_} !_ _%I /.
+Global Arguments bi_absorbingly_if {_} !_ _%_I /.
 Global Instance: Params (@bi_absorbingly_if) 2 := {}.
 Global Typeclasses Opaque bi_absorbingly_if.
 Notation "'<absorb>?' p P" := (bi_absorbingly_if p P) : bi_scope.
 
 Definition bi_intuitionistically {PROP : bi} (P : PROP) : PROP :=
   (<affine> <pers> P)%I.
-Global Arguments bi_intuitionistically {_} _%I : simpl never.
+Global Arguments bi_intuitionistically {_} _%_I : simpl never.
 Global Instance: Params (@bi_intuitionistically) 1 := {}.
 Global Typeclasses Opaque bi_intuitionistically.
 Notation "□ P" := (bi_intuitionistically P) : bi_scope.
 
 Definition bi_intuitionistically_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
   (if p then □ P else P)%I.
-Global Arguments bi_intuitionistically_if {_} !_ _%I /.
+Global Arguments bi_intuitionistically_if {_} !_ _%_I /.
 Global Instance: Params (@bi_intuitionistically_if) 2 := {}.
 Global Typeclasses Opaque bi_intuitionistically_if.
 Notation "'□?' p P" := (bi_intuitionistically_if p P) : bi_scope.
@@ -89,12 +89,12 @@ Fixpoint bi_laterN {PROP : bi} (n : nat) (P : PROP) : PROP :=
   | S n' => ▷ ▷^n' P
   end
 where "▷^ n P" := (bi_laterN n P) : bi_scope.
-Global Arguments bi_laterN {_} !_%nat_scope _%I.
+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.
-Global Arguments bi_except_0 {_} _%I : simpl never.
+Global Arguments bi_except_0 {_} _%_I : simpl never.
 Notation "◇ P" := (bi_except_0 P) : bi_scope.
 Global Instance: Params (@bi_except_0) 1 := {}.
 Global Typeclasses Opaque bi_except_0.
@@ -115,8 +115,8 @@ Global Typeclasses Opaque bi_except_0.
    The law [timeless_alt] in [derived_laws_later.v] provides option two, by
    proving that both versions are equivalent in the logic.  *)
 Class Timeless {PROP : bi} (P : PROP) := timeless : ▷ P ⊢ ◇ P.
-Global Arguments Timeless {_} _%I : simpl never.
-Global Arguments timeless {_} _%I {_}.
+Global Arguments Timeless {_} _%_I : simpl never.
+Global Arguments timeless {_} _%_I {_}.
 Global Hint Mode Timeless + ! : typeclass_instances.
 Global Instance: Params (@Timeless) 1 := {}.
 Global Hint Extern 100 (Timeless (match ?x with _ => _ end)) =>
@@ -130,6 +130,6 @@ Definition bi_wandM {PROP : bi} (mP : option PROP) (Q : PROP) : PROP :=
   | None => Q
   | Some P => P -∗ Q
   end.
-Global Arguments bi_wandM {_} !_%I _%I /.
+Global Arguments bi_wandM {_} !_%_I _%_I /.
 Notation "mP -∗? Q" := (bi_wandM mP Q)
   (at level 99, Q at level 200, right associativity) : bi_scope.
diff --git a/iris/bi/embedding.v b/iris/bi/embedding.v
index 95d08b51ec7e9ac00a2281266d2ef2f79aeb50c3..1ac8fe3d3bbe29ad7decf46fa809d3bacf3f7b9f 100644
--- a/iris/bi/embedding.v
+++ b/iris/bi/embedding.v
@@ -12,7 +12,7 @@ Local Set Primitive Projections.
 Set Default Proof Using "Type*".
 
 Class Embed (A B : Type) := embed : A → B.
-Global Arguments embed {_ _ _} _%I : simpl never.
+Global Arguments embed {_ _ _} _%_I : simpl never.
 Notation "⎡ P ⎤" := (embed P) : bi_scope.
 Global Instance: Params (@embed) 3 := {}.
 Global Typeclasses Opaque embed.
diff --git a/iris/bi/interface.v b/iris/bi/interface.v
index 54ed9441f1a6bcdd4ca1580cefb4a6a237c47fad..d30908d9f3e52d216412b97ec33d26a28393ad2d 100644
--- a/iris/bi/interface.v
+++ b/iris/bi/interface.v
@@ -308,12 +308,12 @@ Global Arguments bi_dist : simpl never.
 Global Arguments bi_equiv : simpl never.
 Global Arguments bi_entails {PROP} _ _ : simpl never, rename.
 Global Arguments bi_emp {PROP} : simpl never, rename.
-Global Arguments bi_pure {PROP} _%stdpp : simpl never, rename.
+Global Arguments bi_pure {PROP} _%_stdpp : simpl never, rename.
 Global Arguments bi_and {PROP} _ _ : simpl never, rename.
 Global Arguments bi_or {PROP} _ _ : simpl never, rename.
 Global Arguments bi_impl {PROP} _ _ : simpl never, rename.
-Global Arguments bi_forall {PROP _} _%I : simpl never, rename.
-Global Arguments bi_exist {PROP _} _%I : simpl never, rename.
+Global Arguments bi_forall {PROP _} _%_I : simpl never, rename.
+Global Arguments bi_exist {PROP _} _%_I : simpl never, rename.
 Global Arguments bi_sep {PROP} _ _ : simpl never, rename.
 Global Arguments bi_wand {PROP} _ _ : simpl never, rename.
 Global Arguments bi_persistently {PROP} _ : simpl never, rename.
@@ -362,7 +362,7 @@ Notation "(.⊣⊢ Q )" := (λ P, P ≡@{bi_car _} Q) (only parsing) : stdpp_sco
 
 Definition bi_emp_valid {PROP : bi} (P : PROP) : Prop := emp ⊢ P.
 
-Global Arguments bi_emp_valid {_} _%I : simpl never.
+Global Arguments bi_emp_valid {_} _%_I : simpl never.
 Global Typeclasses Opaque bi_emp_valid.
 
 Notation "⊢ Q" := (bi_emp_valid Q%I) : stdpp_scope.
diff --git a/iris/bi/lib/counterexamples.v b/iris/bi/lib/counterexamples.v
index 9f45adc28817328019620440fad2b9194fba09e3..191a7282c38e748a5c4b74049ec56d18a6653907 100644
--- a/iris/bi/lib/counterexamples.v
+++ b/iris/bi/lib/counterexamples.v
@@ -129,7 +129,7 @@ Module inv. Section inv.
 
   (** We have invariants *)
   Context (name : Type) (inv : name → PROP → PROP).
-  Global Arguments inv _ _%I.
+  Global Arguments inv _ _%_I.
   Hypothesis inv_persistent : ∀ i P, Persistent (inv i P).
   Hypothesis inv_alloc : ∀ P, P ⊢ fupd M1 (∃ i, inv i P).
   Hypothesis inv_fupd :
diff --git a/iris/bi/lib/fractional.v b/iris/bi/lib/fractional.v
index 8ee2e23af7ba2a17c9efc3e2ee8ff38d420079b3..7043088d7ee0ab1175626e9e439075a0e2dd3778 100644
--- a/iris/bi/lib/fractional.v
+++ b/iris/bi/lib/fractional.v
@@ -4,7 +4,7 @@ From iris.prelude Require Import options.
 
 Class Fractional {PROP : bi} (Φ : Qp → PROP) :=
   fractional p q : Φ (p + q)%Qp ⊣⊢ Φ p ∗ Φ q.
-Global Arguments Fractional {_} _%I : simpl never.
+Global Arguments Fractional {_} _%_I : simpl never.
 Global Arguments fractional {_ _ _} _ _.
 
 (** The [AsFractional] typeclass eta-expands a proposition [P] into [Φ q] such
@@ -23,7 +23,7 @@ Class AsFractional {PROP : bi} (P : PROP) (Φ : Qp → PROP) (q : Qp) := {
   as_fractional : P ⊣⊢ Φ q;
   as_fractional_fractional : Fractional Φ
 }.
-Global Arguments AsFractional {_} _%I _%I _%Qp.
+Global Arguments AsFractional {_} _%_I _%_I _%_Qp.
 Global Hint Mode AsFractional - ! - - : typeclass_instances.
 
 (** The class [FrameFractionalQp] is used for fractional framing, it subtracts
diff --git a/iris/bi/lib/laterable.v b/iris/bi/lib/laterable.v
index 1a03007f724512b6c5a06b72a8c0f36fcda71f4d..0656296772c924b4b16a160b310a1cda7f4de239 100644
--- a/iris/bi/lib/laterable.v
+++ b/iris/bi/lib/laterable.v
@@ -5,8 +5,8 @@ From iris.prelude Require Import options.
 (** The class of laterable assertions *)
 Class Laterable {PROP : bi} (P : PROP) := laterable :
   P ⊢ ∃ Q, ▷ Q ∗ □ (▷ Q -∗ ◇ P).
-Global Arguments Laterable {_} _%I : simpl never.
-Global Arguments laterable {_} _%I {_}.
+Global Arguments Laterable {_} _%_I : simpl never.
+Global Arguments laterable {_} _%_I {_}.
 Global Hint Mode Laterable + ! : typeclass_instances.
 
 (** Proofmode class for turning [P] into a laterable [Q].
@@ -19,9 +19,9 @@ Class IntoLaterable {PROP : bi} (P Q : PROP) : Prop := {
   into_laterable : P ⊢ Q;
   into_laterable_result_laterable : Laterable Q;
 }.
-Global Arguments IntoLaterable {_} P%I Q%I.
-Global Arguments into_laterable {_} P%I Q%I {_}.
-Global Arguments into_laterable_result_laterable {_} P%I Q%I {_}.
+Global Arguments IntoLaterable {_} P%_I Q%_I.
+Global Arguments into_laterable {_} P%_I Q%_I {_}.
+Global Arguments into_laterable_result_laterable {_} P%_I Q%_I {_}.
 Global Hint Mode IntoLaterable + ! - : typeclass_instances.
 
 Section instances.
diff --git a/iris/bi/monpred.v b/iris/bi/monpred.v
index 0b6b9a07f8f1474c343356ea17802172bb054e6b..5ad957e8d4fd4f9d587a6fe0de0382383c617879 100644
--- a/iris/bi/monpred.v
+++ b/iris/bi/monpred.v
@@ -108,7 +108,7 @@ Section cofe.
 End cofe.
 
 Global Arguments monPred _ _ : clear implicits.
-Global Arguments monPred_at {_ _} _%I _.
+Global Arguments monPred_at {_ _} _%_I _.
 Local Existing Instance monPred_mono.
 Global Arguments monPredO _ _ : clear implicits.
 
@@ -305,8 +305,8 @@ Local Definition monPred_unseal :=
    @monPred_in_unseal, @monPred_later_unseal).
 End monPred_defs.
 
-Global Arguments monPred_objectively {_ _} _%I.
-Global Arguments monPred_subjectively {_ _} _%I.
+Global Arguments monPred_objectively {_ _} _%_I.
+Global Arguments monPred_subjectively {_ _} _%_I.
 Notation "'<obj>' P" := (monPred_objectively P) : bi_scope.
 Notation "'<subj>' P" := (monPred_subjectively P) : bi_scope.
 
@@ -667,8 +667,8 @@ End monPred.
 
 Class Objective {I : biIndex} {PROP : bi} (P : monPred I PROP) :=
   objective_at i j : P i ⊢ P j.
-Global Arguments Objective {_ _} _%I.
-Global Arguments objective_at {_ _} _%I {_}.
+Global Arguments Objective {_ _} _%_I.
+Global Arguments objective_at {_ _} _%_I {_}.
 Global Hint Mode Objective + + ! : typeclass_instances.
 Global Instance: Params (@Objective) 2 := {}.
 
diff --git a/iris/bi/plainly.v b/iris/bi/plainly.v
index abd3792f30f7a42fcbb9bf98fb9bd42a4c672df3..6bb0e1db7df4fc5a57a72b0ed88c76f2f9d548d8 100644
--- a/iris/bi/plainly.v
+++ b/iris/bi/plainly.v
@@ -12,7 +12,7 @@ Local Set Primitive Projections.
 Set Default Proof Using "Type*".
 
 Class Plainly (PROP : Type) := plainly : PROP → PROP.
-Global Arguments plainly {PROP}%type_scope {_} _%I.
+Global Arguments plainly {PROP}%_type_scope {_} _%_I.
 Global Hint Mode Plainly ! : typeclass_instances.
 Global Instance: Params (@plainly) 2 := {}.
 Global Typeclasses Opaque plainly.
@@ -103,8 +103,8 @@ End plainly_laws.
 
 (* Derived properties and connectives *)
 Class Plain {PROP: bi} `{!BiPlainly PROP} (P : PROP) := plain : P ⊢ ■ P.
-Global Arguments Plain {_ _} _%I : simpl never.
-Global Arguments plain {_ _} _%I {_}.
+Global Arguments Plain {_ _} _%_I : simpl never.
+Global Arguments plain {_ _} _%_I {_}.
 Global Hint Mode Plain + - ! : typeclass_instances.
 Global Instance: Params (@Plain) 1 := {}.
 Global Hint Extern 100 (Plain (match ?x with _ => _ end)) =>
@@ -112,7 +112,7 @@ Global Hint Extern 100 (Plain (match ?x with _ => _ end)) =>
 
 Definition plainly_if {PROP: bi} `{!BiPlainly PROP} (p : bool) (P : PROP) : PROP :=
   (if p then ■ P else P)%I.
-Global Arguments plainly_if {_ _} !_ _%I /.
+Global Arguments plainly_if {_ _} !_ _%_I /.
 Global Instance: Params (@plainly_if) 2 := {}.
 Global Typeclasses Opaque plainly_if.
 
diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index bded5423ae90762c341636585f6df2c8fd5908bb..9c8198d4731cf452005ae1858679675e0548294d 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -16,7 +16,7 @@ bundle these operational type classes with the laws. *)
 Class BUpd (PROP : Type) : Type := bupd : PROP → PROP.
 Global Instance : Params (@bupd) 2 := {}.
 Global Hint Mode BUpd ! : typeclass_instances.
-Global Arguments bupd {_}%type_scope {_} _%bi_scope.
+Global Arguments bupd {_}%_type_scope {_} _%_bi_scope.
 Global Typeclasses Opaque bupd.
 
 Notation "|==> Q" := (bupd Q) : bi_scope.
@@ -26,7 +26,7 @@ Notation "P ==∗ Q" := (P -∗ |==> Q) : stdpp_scope.
 Class FUpd (PROP : Type) : Type := fupd : coPset → coPset → PROP → PROP.
 Global Instance: Params (@fupd) 4 := {}.
 Global Hint Mode FUpd ! : typeclass_instances.
-Global Arguments fupd {_}%type_scope {_} _ _ _%bi_scope.
+Global Arguments fupd {_}%_type_scope {_} _ _ _%_bi_scope.
 Global Typeclasses Opaque fupd.
 
 Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q) : bi_scope.
diff --git a/iris/bi/weakestpre.v b/iris/bi/weakestpre.v
index b385cf47cfbc6393920a24293dbe698b0065ba2a..6ef42f7217aa7c9e066f7c5b1b95723322e33419 100644
--- a/iris/bi/weakestpre.v
+++ b/iris/bi/weakestpre.v
@@ -34,12 +34,12 @@ different [A], the plan is to generalize the notation to use [Inhabited] instead
 to pick a default value depending on [A]. *)
 Class Wp (PROP EXPR VAL A : Type) :=
   wp : A → coPset → EXPR → (VAL → PROP) → PROP.
-Global Arguments wp {_ _ _ _ _} _ _ _%E _%I.
+Global Arguments wp {_ _ _ _ _} _ _ _%_E _%_I.
 Global Instance: Params (@wp) 8 := {}.
 
 Class Twp (PROP EXPR VAL A : Type) :=
   twp : A → coPset → EXPR → (VAL → PROP) → PROP.
-Global Arguments twp {_ _ _ _ _} _ _ _%E _%I.
+Global Arguments twp {_ _ _ _ _} _ _ _%_E _%_I.
 Global Instance: Params (@twp) 8 := {}.
 
 (** Notations for partial weakest preconditions *)
diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index 67c97ebfc661109b3f37a94fed1db986ec1a32f0..a93f6c3ab421acb4ee4d6987bb61bb96dafde1a1 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -12,26 +12,26 @@ Inductive pm_error (s : string) := .
 
 Class FromAssumption {PROP : bi} (p : bool) (P Q : PROP) :=
   from_assumption : □?p P ⊢ Q.
-Global Arguments FromAssumption {_} _ _%I _%I : simpl never.
-Global Arguments from_assumption {_} _ _%I _%I {_}.
+Global Arguments FromAssumption {_} _ _%_I _%_I : simpl never.
+Global Arguments from_assumption {_} _ _%_I _%_I {_}.
 Global Hint Mode FromAssumption + + - - : typeclass_instances.
 
 Class KnownLFromAssumption {PROP : bi} (p : bool) (P Q : PROP) :=
   #[global] knownl_from_assumption :: FromAssumption p P Q.
-Global Arguments KnownLFromAssumption {_} _ _%I _%I : simpl never.
-Global Arguments knownl_from_assumption {_} _ _%I _%I {_}.
+Global Arguments KnownLFromAssumption {_} _ _%_I _%_I : simpl never.
+Global Arguments knownl_from_assumption {_} _ _%_I _%_I {_}.
 Global Hint Mode KnownLFromAssumption + + ! - : typeclass_instances.
 
 Class KnownRFromAssumption {PROP : bi} (p : bool) (P Q : PROP) :=
   #[global] knownr_from_assumption :: FromAssumption p P Q.
-Global Arguments KnownRFromAssumption {_} _ _%I _%I : simpl never.
-Global Arguments knownr_from_assumption {_} _ _%I _%I {_}.
+Global Arguments KnownRFromAssumption {_} _ _%_I _%_I : simpl never.
+Global Arguments knownr_from_assumption {_} _ _%_I _%_I {_}.
 Global Hint Mode KnownRFromAssumption + + - ! : typeclass_instances.
 
 Class IntoPure {PROP : bi} (P : PROP) (φ : Prop) :=
   into_pure : P ⊢ ⌜φ⌝.
-Global Arguments IntoPure {_} _%I _%type_scope : simpl never.
-Global Arguments into_pure {_} _%I _%type_scope {_}.
+Global Arguments IntoPure {_} _%_I _%_type_scope : simpl never.
+Global Arguments into_pure {_} _%_I _%_type_scope {_}.
 Global Hint Mode IntoPure + ! - : typeclass_instances.
 
 (* [IntoPureT] is a variant of [IntoPure] with the argument in [Type] to avoid
@@ -72,8 +72,8 @@ Note that the Boolean [a] is not needed for the (dual) [IntoPure] class, because
 there we can just ask that [P] is [Affine]. *)
 Class FromPure {PROP : bi} (a : bool) (P : PROP) (φ : Prop) :=
   from_pure : <affine>?a ⌜φ⌝ ⊢ P.
-Global Arguments FromPure {_} _ _%I _%type_scope : simpl never.
-Global Arguments from_pure {_} _ _%I _%type_scope {_}.
+Global Arguments FromPure {_} _ _%_I _%_type_scope : simpl never.
+Global Arguments from_pure {_} _ _%_I _%_type_scope {_}.
 Global Hint Mode FromPure + - ! - : typeclass_instances.
 
 Class FromPureT {PROP : bi} (a : bool) (P : PROP) (φ : Type) :=
@@ -86,14 +86,14 @@ Global Hint Extern 0 (FromPureT _ _ _) =>
 
 Class IntoInternalEq `{BiInternalEq PROP} {A : ofe} (P : PROP) (x y : A) :=
   into_internal_eq : P ⊢ x ≡ y.
-Global Arguments IntoInternalEq {_ _ _} _%I _%type_scope _%type_scope : simpl never.
-Global Arguments into_internal_eq {_ _ _} _%I _%type_scope _%type_scope {_}.
+Global Arguments IntoInternalEq {_ _ _} _%_I _%_type_scope _%_type_scope : simpl never.
+Global Arguments into_internal_eq {_ _ _} _%_I _%_type_scope _%_type_scope {_}.
 Global Hint Mode IntoInternalEq + - - ! - - : typeclass_instances.
 
 Class IntoPersistent {PROP : bi} (p : bool) (P Q : PROP) :=
   into_persistent : <pers>?p P ⊢ <pers> Q.
-Global Arguments IntoPersistent {_} _ _%I _%I : simpl never.
-Global Arguments into_persistent {_} _ _%I _%I {_}.
+Global Arguments IntoPersistent {_} _ _%_I _%_I : simpl never.
+Global Arguments into_persistent {_} _ _%_I _%_I {_}.
 Global Hint Mode IntoPersistent + + ! - : typeclass_instances.
 
 (** The [FromModal φ M sel P Q] class is used by the [iModIntro] tactic to
@@ -116,8 +116,8 @@ modalities [N] are [bupd], [fupd], [except_0], [monPred_subjectively] and
 Class FromModal {PROP1 PROP2 : bi} {A}
     (φ : Prop) (M : modality PROP1 PROP2) (sel : A) (P : PROP2) (Q : PROP1) :=
   from_modal : φ → M Q ⊢ P.
-Global Arguments FromModal {_ _ _} _ _ _%I _%I _%I : simpl never.
-Global Arguments from_modal {_ _ _} _ _ _ _%I _%I {_}.
+Global Arguments FromModal {_ _ _} _ _ _%_I _%_I _%_I : simpl never.
+Global Arguments from_modal {_ _ _} _ _ _ _%_I _%_I {_}.
 Global Hint Mode FromModal - + - - - - ! - : typeclass_instances.
 
 (** The [FromAffinely P Q] class is used to add an [<affine>] modality to the
@@ -126,8 +126,8 @@ proposition [Q].
 The input is [Q] and the output is [P]. *)
 Class FromAffinely {PROP : bi} (P Q : PROP) :=
   from_affinely : <affine> Q ⊢ P.
-Global Arguments FromAffinely {_} _%I _%I : simpl never.
-Global Arguments from_affinely {_} _%I _%I {_}.
+Global Arguments FromAffinely {_} _%_I _%_I : simpl never.
+Global Arguments from_affinely {_} _%_I _%_I {_}.
 Global Hint Mode FromAffinely + - ! : typeclass_instances.
 
 (** The [IntoAbsorbingly P Q] class is used to add an [<absorb>] modality to
@@ -136,8 +136,8 @@ the proposition [Q].
 The input is [Q] and the output is [P]. *)
 Class IntoAbsorbingly {PROP : bi} (P Q : PROP) :=
   into_absorbingly : P ⊢ <absorb> Q.
-Global Arguments IntoAbsorbingly {_} _%I _%I.
-Global Arguments into_absorbingly {_} _%I _%I {_}.
+Global Arguments IntoAbsorbingly {_} _%_I _%_I.
+Global Arguments into_absorbingly {_} _%_I _%_I {_}.
 Global Hint Mode IntoAbsorbingly + - ! : typeclass_instances.
 
 (** Converting an assumption [R] into a wand [P -∗ Q] is done in three stages:
@@ -150,34 +150,34 @@ Global Hint Mode IntoAbsorbingly + - ! : typeclass_instances.
 - Instantiate the premise of the wand or implication. *)
 Class IntoWand {PROP : bi} (p q : bool) (R P Q : PROP) :=
   into_wand : □?p R ⊢ □?q P -∗ Q.
-Global Arguments IntoWand {_} _ _ _%I _%I _%I : simpl never.
-Global Arguments into_wand {_} _ _ _%I _%I _%I {_}.
+Global Arguments IntoWand {_} _ _ _%_I _%_I _%_I : simpl never.
+Global Arguments into_wand {_} _ _ _%_I _%_I _%_I {_}.
 Global Hint Mode IntoWand + + + ! - - : typeclass_instances.
 
 Class IntoWand' {PROP : bi} (p q : bool) (R P Q : PROP) :=
   into_wand' : IntoWand p q R P Q.
-Global Arguments IntoWand' {_} _ _ _%I _%I _%I : simpl never.
+Global Arguments IntoWand' {_} _ _ _%_I _%_I _%_I : simpl never.
 Global Hint Mode IntoWand' + + + ! ! - : typeclass_instances.
 Global Hint Mode IntoWand' + + + ! - ! : typeclass_instances.
 
 Class FromWand {PROP : bi} (P Q1 Q2 : PROP) := from_wand : (Q1 -∗ Q2) ⊢ P.
-Global Arguments FromWand {_} _%I _%I _%I : simpl never.
-Global Arguments from_wand {_} _%I _%I _%I {_}.
+Global Arguments FromWand {_} _%_I _%_I _%_I : simpl never.
+Global Arguments from_wand {_} _%_I _%_I _%_I {_}.
 Global Hint Mode FromWand + ! - - : typeclass_instances.
 
 Class FromImpl {PROP : bi} (P Q1 Q2 : PROP) := from_impl : (Q1 → Q2) ⊢ P.
-Global Arguments FromImpl {_} _%I _%I _%I : simpl never.
-Global Arguments from_impl {_} _%I _%I _%I {_}.
+Global Arguments FromImpl {_} _%_I _%_I _%_I : simpl never.
+Global Arguments from_impl {_} _%_I _%_I _%_I {_}.
 Global Hint Mode FromImpl + ! - - : typeclass_instances.
 
 Class FromSep {PROP : bi} (P Q1 Q2 : PROP) := from_sep : Q1 ∗ Q2 ⊢ P.
-Global Arguments FromSep {_} _%I _%I _%I : simpl never.
-Global Arguments from_sep {_} _%I _%I _%I {_}.
+Global Arguments FromSep {_} _%_I _%_I _%_I : simpl never.
+Global Arguments from_sep {_} _%_I _%_I _%_I {_}.
 Global Hint Mode FromSep + ! - - : typeclass_instances. (* For iSplit{L,R} *)
 
 Class FromAnd {PROP : bi} (P Q1 Q2 : PROP) := from_and : Q1 ∧ Q2 ⊢ P.
-Global Arguments FromAnd {_} _%I _%I _%I : simpl never.
-Global Arguments from_and {_} _%I _%I _%I {_}.
+Global Arguments FromAnd {_} _%_I _%_I _%_I : simpl never.
+Global Arguments from_and {_} _%_I _%_I _%_I {_}.
 Global Hint Mode FromAnd + ! - - : typeclass_instances.
 
 (** The [IntoAnd p P Q1 Q2] class is used to handle some [[H1 H2]] intro
@@ -190,8 +190,8 @@ patterns:
 The inputs are [p P] and the outputs are [Q1 Q2]. *)
 Class IntoAnd {PROP : bi} (p : bool) (P Q1 Q2 : PROP) :=
   into_and : □?p P ⊢ □?p (Q1 ∧ Q2).
-Global Arguments IntoAnd {_} _ _%I _%I _%I : simpl never.
-Global Arguments into_and {_} _ _%I _%I _%I {_}.
+Global Arguments IntoAnd {_} _ _%_I _%_I _%_I : simpl never.
+Global Arguments into_and {_} _ _%_I _%_I _%_I {_}.
 Global Hint Mode IntoAnd + + ! - - : typeclass_instances.
 
 (** The [IntoSep P Q1 Q2] class is used to handle [[H1 H2]] intro patterns in
@@ -203,47 +203,47 @@ the spatial context, except:
 The input is [P] and the outputs are [Q1 Q2]. *)
 Class IntoSep {PROP : bi} (P Q1 Q2 : PROP) :=
   into_sep : P ⊢ Q1 ∗ Q2.
-Global Arguments IntoSep {_} _%I _%I _%I : simpl never.
-Global Arguments into_sep {_} _%I _%I _%I {_}.
+Global Arguments IntoSep {_} _%_I _%_I _%_I : simpl never.
+Global Arguments into_sep {_} _%_I _%_I _%_I {_}.
 Global Hint Mode IntoSep + ! - - : typeclass_instances.
 
 Class FromOr {PROP : bi} (P Q1 Q2 : PROP) := from_or : Q1 ∨ Q2 ⊢ P.
-Global Arguments FromOr {_} _%I _%I _%I : simpl never.
-Global Arguments from_or {_} _%I _%I _%I {_}.
+Global Arguments FromOr {_} _%_I _%_I _%_I : simpl never.
+Global Arguments from_or {_} _%_I _%_I _%_I {_}.
 Global Hint Mode FromOr + ! - - : typeclass_instances.
 
 Class IntoOr {PROP : bi} (P Q1 Q2 : PROP) := into_or : P ⊢ Q1 ∨ Q2.
-Global Arguments IntoOr {_} _%I _%I _%I : simpl never.
-Global Arguments into_or {_} _%I _%I _%I {_}.
+Global Arguments IntoOr {_} _%_I _%_I _%_I : simpl never.
+Global Arguments into_or {_} _%_I _%_I _%_I {_}.
 Global Hint Mode IntoOr + ! - - : typeclass_instances.
 
 Class FromExist {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :=
   from_exist : (∃ x, Φ x) ⊢ P.
-Global Arguments FromExist {_ _} _%I _%I : simpl never.
-Global Arguments from_exist {_ _} _%I _%I {_}.
+Global Arguments FromExist {_ _} _%_I _%_I : simpl never.
+Global Arguments from_exist {_ _} _%_I _%_I {_}.
 Global Hint Mode FromExist + - ! - : typeclass_instances.
 
 Class IntoExist {PROP : bi} {A} (P : PROP) (Φ : A → PROP) (name: ident_name) :=
   into_exist : P ⊢ ∃ x, Φ x.
-Global Arguments IntoExist {_ _} _%I _%I _ : simpl never.
-Global Arguments into_exist {_ _} _%I _%I _ {_}.
+Global Arguments IntoExist {_ _} _%_I _%_I _ : simpl never.
+Global Arguments into_exist {_ _} _%_I _%_I _ {_}.
 Global Hint Mode IntoExist + - ! - - : typeclass_instances.
 
 Class IntoForall {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :=
   into_forall : P ⊢ ∀ x, Φ x.
-Global Arguments IntoForall {_ _} _%I _%I : simpl never.
-Global Arguments into_forall {_ _} _%I _%I {_}.
+Global Arguments IntoForall {_ _} _%_I _%_I : simpl never.
+Global Arguments into_forall {_ _} _%_I _%_I {_}.
 Global Hint Mode IntoForall + - ! - : typeclass_instances.
 
 Class FromForall {PROP : bi} {A} (P : PROP) (Φ : A → PROP) (name : ident_name) :=
   from_forall : (∀ x, Φ x) ⊢ P.
-Global Arguments FromForall {_ _} _%I _%I _ : simpl never.
-Global Arguments from_forall {_ _} _%I _%I _ {_}.
+Global Arguments FromForall {_ _} _%_I _%_I _ : simpl never.
+Global Arguments from_forall {_ _} _%_I _%_I _ {_}.
 Global Hint Mode FromForall + - ! - - : typeclass_instances.
 
 Class IsExcept0 {PROP : bi} (Q : PROP) := is_except_0 : ◇ Q ⊢ Q.
-Global Arguments IsExcept0 {_} _%I : simpl never.
-Global Arguments is_except_0 {_} _%I {_}.
+Global Arguments IsExcept0 {_} _%_I : simpl never.
+Global Arguments is_except_0 {_} _%_I {_}.
 Global Hint Mode IsExcept0 + ! : typeclass_instances.
 
 (** [CombineSepAs], [MaybeCombineSepAs] and [CombineSepGives] are all used for
@@ -279,8 +279,8 @@ In terms of costs, note that the [AsFractional] instance for [CombineSepAs]
 has cost 50. If that instance should take priority over yours, make sure to use
 a higher cost. *)
 Class CombineSepAs {PROP : bi} (P Q R : PROP) := combine_sep_as : P ∗ Q ⊢ R.
-Global Arguments CombineSepAs {_} _%I _%I _%I : simpl never.
-Global Arguments combine_sep_as {_} _%I _%I _%I {_}.
+Global Arguments CombineSepAs {_} _%_I _%_I _%_I : simpl never.
+Global Arguments combine_sep_as {_} _%_I _%_I _%_I {_}.
 Global Hint Mode CombineSepAs + ! ! - : typeclass_instances.
 
 (** The [progress] parameter is of the following [progress_indicator] type: *)
@@ -292,8 +292,8 @@ indicates that a [CombineSepAs] instance was used. *)
 Class MaybeCombineSepAs {PROP : bi}
     (P Q R : PROP) (progress : progress_indicator) :=
   maybe_combine_sep_as : P ∗ Q ⊢ R.
-Global Arguments MaybeCombineSepAs {_} _%I _%I _%I _ : simpl never.
-Global Arguments maybe_combine_sep_as {_} _%I _%I _%I _ {_}.
+Global Arguments MaybeCombineSepAs {_} _%_I _%_I _%_I _ : simpl never.
+Global Arguments maybe_combine_sep_as {_} _%_I _%_I _%_I _ {_}.
 Global Hint Mode MaybeCombineSepAs + ! ! - - : typeclass_instances.
 
 Global Instance maybe_combine_sep_as_combine_sep_as {PROP : bi} (R P Q : PROP) :
@@ -311,8 +311,8 @@ non-trivial information. If such information cannot be found, we want to
 produce an error, instead of the trivial hypothesis [True]. *)
 Class CombineSepGives {PROP : bi} (P Q R : PROP) :=
   combine_sep_gives : P ∗ Q ⊢ <pers> R.
-Global Arguments CombineSepGives {_} _%I _%I _%I : simpl never.
-Global Arguments combine_sep_gives {_} _%I _%I _%I {_}.
+Global Arguments CombineSepGives {_} _%_I _%_I _%_I : simpl never.
+Global Arguments combine_sep_gives {_} _%_I _%_I _%_I {_}.
 Global Hint Mode CombineSepGives + ! ! - : typeclass_instances.
 
 (** The [ElimModal φ p p' P P' Q Q'] class is used by the [iMod] tactic.
@@ -336,16 +336,16 @@ originally). A corresponding [ElimModal] instance for the Iris 1/2-style update
 modality, would have a side-condition [φ] on the masks. *)
 Class ElimModal {PROP : bi} (φ : Prop) (p p' : bool) (P P' : PROP) (Q Q' : PROP) :=
   elim_modal : φ → □?p P ∗ (□?p' P' -∗ Q') ⊢ Q.
-Global Arguments ElimModal {_} _ _ _ _%I _%I _%I _%I : simpl never.
-Global Arguments elim_modal {_} _ _ _ _%I _%I _%I _%I {_}.
+Global Arguments ElimModal {_} _ _ _ _%_I _%_I _%_I _%_I : simpl never.
+Global Arguments elim_modal {_} _ _ _ _%_I _%_I _%_I _%_I {_}.
 Global Hint Mode ElimModal + - ! - ! - ! - : typeclass_instances.
 
 (* Used by the specialization pattern [ > ] in [iSpecialize] and [iAssert] to
 add a modality to the goal corresponding to a premise/asserted proposition. *)
 Class AddModal {PROP : bi} (P P' : PROP) (Q : PROP) :=
   add_modal : P ∗ (P' -∗ Q) ⊢ Q.
-Global Arguments AddModal {_} _%I _%I _%I : simpl never.
-Global Arguments add_modal {_} _%I _%I _%I {_}.
+Global Arguments AddModal {_} _%_I _%_I _%_I : simpl never.
+Global Arguments add_modal {_} _%_I _%_I _%_I {_}.
 Global Hint Mode AddModal + - ! ! : typeclass_instances.
 
 Lemma add_modal_id {PROP : bi} (P Q : PROP) : AddModal P P Q.
@@ -374,8 +374,8 @@ Global Instance is_disj_union_disj_union `{DisjUnion A} (X1 X2 : A) :
 Proof. done. Qed.
 
 Class Frame {PROP : bi} (p : bool) (R P Q : PROP) := frame : □?p R ∗ Q ⊢ P.
-Global Arguments Frame {_} _ _%I _%I _%I.
-Global Arguments frame {_} _ _%I _%I _%I {_}.
+Global Arguments Frame {_} _ _%_I _%_I _%_I.
+Global Arguments frame {_} _ _%_I _%_I _%_I {_}.
 Global Hint Mode Frame + + ! ! - : typeclass_instances.
 
 (* The boolean [progress] indicates whether actual framing has been performed.
@@ -385,8 +385,8 @@ used.
 the [MaybeFrame] notation defined below. *)
 Class MaybeFrame' {PROP : bi} (p : bool) (R P Q : PROP) (progress : bool) :=
   maybe_frame : □?p R ∗ Q ⊢ P.
-Global Arguments MaybeFrame' {_} _ _%I _%I _%I _.
-Global Arguments maybe_frame {_} _ _%I _%I _%I _ {_}.
+Global Arguments MaybeFrame' {_} _ _%_I _%_I _%_I _.
+Global Arguments maybe_frame {_} _ _%_I _%_I _%_I _ {_}.
 Global Hint Mode MaybeFrame' + + ! - - - : typeclass_instances.
 
 Global Instance maybe_frame_frame {PROP : bi} p (R P Q : PROP) :
@@ -433,8 +433,8 @@ found, the addition of [FrameInstantiateExistDisabled] to the context disables
 the instantiation of existential quantifiers. *)
 
 Class IntoExcept0 {PROP : bi} (P Q : PROP) := into_except_0 : P ⊢ ◇ Q.
-Global Arguments IntoExcept0 {_} _%I _%I : simpl never.
-Global Arguments into_except_0 {_} _%I _%I {_}.
+Global Arguments IntoExcept0 {_} _%_I _%_I : simpl never.
+Global Arguments into_except_0 {_} _%_I _%_I {_}.
 Global Hint Mode IntoExcept0 + ! - : typeclass_instances.
 Global Hint Mode IntoExcept0 + - ! : typeclass_instances.
 
@@ -474,13 +474,13 @@ Proof. iIntros "H". iFrame "H". Qed.
 *)
 Class MaybeIntoLaterN {PROP : bi} (only_head : bool) (n : nat) (P Q : PROP) :=
   maybe_into_laterN : P ⊢ ▷^n Q.
-Global Arguments MaybeIntoLaterN {_} _ _%nat_scope _%I _%I.
-Global Arguments maybe_into_laterN {_} _ _%nat_scope _%I _%I {_}.
+Global Arguments MaybeIntoLaterN {_} _ _%_nat_scope _%_I _%_I.
+Global Arguments maybe_into_laterN {_} _ _%_nat_scope _%_I _%_I {_}.
 Global Hint Mode MaybeIntoLaterN + + + - - : typeclass_instances.
 
 Class IntoLaterN {PROP : bi} (only_head : bool) (n : nat) (P Q : PROP) :=
   #[global] into_laterN :: MaybeIntoLaterN only_head n P Q.
-Global Arguments IntoLaterN {_} _ _%nat_scope _%I _%I.
+Global Arguments IntoLaterN {_} _ _%_nat_scope _%_I _%_I.
 Global Hint Mode IntoLaterN + + + ! - : typeclass_instances.
 
 Global Instance maybe_into_laterN_default {PROP : bi} only_head n (P : PROP) :
@@ -499,8 +499,8 @@ embeddings using [iModIntro].
 Input: the proposition [P], output: the proposition [Q] so that [P ⊢ ⎡Q⎤]. *)
 Class IntoEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP') (Q : PROP) :=
   into_embed : P ⊢ ⎡Q⎤.
-Global Arguments IntoEmbed {_ _ _} _%I _%I.
-Global Arguments into_embed {_ _ _} _%I _%I {_}.
+Global Arguments IntoEmbed {_ _ _} _%_I _%_I.
+Global Arguments into_embed {_ _ _} _%_I _%_I {_}.
 Global Hint Mode IntoEmbed + + + ! -  : typeclass_instances.
 
 (* We use two type classes for [AsEmpValid], in order to avoid loops in
@@ -517,10 +517,10 @@ Global Hint Mode IntoEmbed + + + ! -  : typeclass_instances.
    projections for hints modes would make this fail.*)
 Class AsEmpValid {PROP : bi} (φ : Prop) (P : PROP) :=
   as_emp_valid : φ ↔ ⊢ P.
-Global Arguments AsEmpValid {_} _%type _%I.
+Global Arguments AsEmpValid {_} _%_type _%_I.
 Class AsEmpValid0 {PROP : bi} (φ : Prop) (P : PROP) :=
   as_emp_valid_0 : AsEmpValid φ P.
-Global Arguments AsEmpValid0 {_} _%type _%I.
+Global Arguments AsEmpValid0 {_} _%_type _%_I.
 Global Existing Instance as_emp_valid_0 | 0.
 
 Lemma as_emp_valid_1 (φ : Prop) {PROP : bi} (P : PROP) `{!AsEmpValid φ P} :
@@ -533,7 +533,7 @@ Proof. by apply as_emp_valid. Qed.
 (* Input: [P]; Outputs: [N],
    Extracts the namespace associated with an invariant assertion. Used for [iInv]. *)
 Class IntoInv {PROP : bi} (P: PROP) (N: namespace).
-Global Arguments IntoInv {_} _%I _.
+Global Arguments IntoInv {_} _%_I _.
 Global Hint Mode IntoInv + ! - : typeclass_instances.
 
 (** Accessors.
@@ -556,8 +556,8 @@ Class ElimAcc {PROP : bi} {X : Type} (φ : Prop) (M1 M2 : PROP → PROP)
       (α β : X → PROP) (mγ : X → option PROP)
       (Q : PROP) (Q' : X → PROP) :=
   elim_acc : φ → ((∀ x, α x -∗ Q' x) -∗ accessor M1 M2 α β mγ -∗ Q).
-Global Arguments ElimAcc {_} {_} _ _%I _%I _%I _%I _%I _%I : simpl never.
-Global Arguments elim_acc {_} {_} _ _%I _%I _%I _%I _%I _%I {_}.
+Global Arguments ElimAcc {_} {_} _ _%_I _%_I _%_I _%_I _%_I _%_I : simpl never.
+Global Arguments elim_acc {_} {_} _ _%_I _%_I _%_I _%_I _%_I _%_I {_}.
 Global Hint Mode ElimAcc + ! - ! ! ! ! ! ! - : typeclass_instances.
 
 (* Turn [P] into an accessor.
@@ -573,8 +573,8 @@ Global Hint Mode ElimAcc + ! - ! ! ! ! ! ! - : typeclass_instances.
 Class IntoAcc {PROP : bi} {X : Type} (Pacc : PROP) (φ : Prop) (Pin : PROP)
       (M1 M2 : PROP → PROP) (α β : X → PROP) (mγ : X → option PROP) :=
   into_acc : φ → Pacc -∗ Pin -∗ accessor M1 M2 α β mγ.
-Global Arguments IntoAcc {_} {_} _%I _ _%I _%I _%I _%I _%I _%I : simpl never.
-Global Arguments into_acc {_} {_} _%I _ _%I _%I _%I _%I _%I _%I {_} : simpl never.
+Global Arguments IntoAcc {_} {_} _%_I _ _%_I _%_I _%_I _%_I _%_I _%_I : simpl never.
+Global Arguments into_acc {_} {_} _%_I _ _%_I _%_I _%_I _%_I _%_I _%_I {_} : simpl never.
 Global Hint Mode IntoAcc + - ! - - - - - - - : typeclass_instances.
 
 (* The typeclass used for the [iInv] tactic.
@@ -599,8 +599,8 @@ Class ElimInv {PROP : bi} {X : Type} (φ : Prop)
       (Pinv Pin : PROP) (Pout : X → PROP) (mPclose : option (X → PROP))
       (Q : PROP) (Q' : X → PROP) :=
   elim_inv : φ → Pinv ∗ Pin ∗ (∀ x, Pout x ∗ (default (λ _, emp) mPclose) x -∗ Q' x) ⊢ Q.
-Global Arguments ElimInv {_} {_} _ _%I _%I _%I _%I _%I _%I : simpl never.
-Global Arguments elim_inv {_} {_} _ _%I _%I _%I _%I _%I _%I {_}.
+Global Arguments ElimInv {_} {_} _ _%_I _%_I _%_I _%_I _%_I _%_I : simpl never.
+Global Arguments elim_inv {_} {_} _ _%_I _%_I _%_I _%_I _%_I _%_I {_}.
 Global Hint Mode ElimInv + - - ! - - ! ! - : typeclass_instances.
 
 (** We make sure that tactics that perform actions on *specific* hypotheses or
diff --git a/iris/proofmode/classes_make.v b/iris/proofmode/classes_make.v
index c173bfd2f5bbd1ae75381020f390e64f76ebf5d5..0d8ef22c89efbcd6be5eeb385bf3714b85ed9739 100644
--- a/iris/proofmode/classes_make.v
+++ b/iris/proofmode/classes_make.v
@@ -52,98 +52,98 @@ Global Hint Mode QuickAbsorbing + ! : typeclass_instances.
 
 Class MakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
   make_embed : ⎡P⎤ ⊣⊢ Q.
-Global Arguments MakeEmbed {_ _ _} _%I _%I.
+Global Arguments MakeEmbed {_ _ _} _%_I _%_I.
 Global Hint Mode MakeEmbed + + + - - : typeclass_instances.
 Class KnownMakeEmbed {PROP PROP' : bi} `{BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
   #[global] known_make_embed :: MakeEmbed P Q.
-Global Arguments KnownMakeEmbed {_ _ _} _%I _%I.
+Global Arguments KnownMakeEmbed {_ _ _} _%_I _%_I.
 Global Hint Mode KnownMakeEmbed + + + ! - : typeclass_instances.
 
 Class MakeSep {PROP : bi} (P Q PQ : PROP) := make_sep : P ∗ Q ⊣⊢ PQ .
-Global Arguments MakeSep {_} _%I _%I _%I.
+Global Arguments MakeSep {_} _%_I _%_I _%_I.
 Global Hint Mode MakeSep + - - - : typeclass_instances.
 Class KnownLMakeSep {PROP : bi} (P Q PQ : PROP) :=
   #[global] knownl_make_sep :: MakeSep P Q PQ.
-Global Arguments KnownLMakeSep {_} _%I _%I _%I.
+Global Arguments KnownLMakeSep {_} _%_I _%_I _%_I.
 Global Hint Mode KnownLMakeSep + ! - - : typeclass_instances.
 Class KnownRMakeSep {PROP : bi} (P Q PQ : PROP) :=
   #[global] knownr_make_sep :: MakeSep P Q PQ.
-Global Arguments KnownRMakeSep {_} _%I _%I _%I.
+Global Arguments KnownRMakeSep {_} _%_I _%_I _%_I.
 Global Hint Mode KnownRMakeSep + - ! - : typeclass_instances.
 
 Class MakeAnd {PROP : bi} (P Q PQ : PROP) :=  make_and_l : P ∧ Q ⊣⊢ PQ.
-Global Arguments MakeAnd {_} _%I _%I _%I.
+Global Arguments MakeAnd {_} _%_I _%_I _%_I.
 Global Hint Mode MakeAnd + - - - : typeclass_instances.
 Class KnownLMakeAnd {PROP : bi} (P Q PQ : PROP) :=
   #[global] knownl_make_and :: MakeAnd P Q PQ.
-Global Arguments KnownLMakeAnd {_} _%I _%I _%I.
+Global Arguments KnownLMakeAnd {_} _%_I _%_I _%_I.
 Global Hint Mode KnownLMakeAnd + ! - - : typeclass_instances.
 Class KnownRMakeAnd {PROP : bi} (P Q PQ : PROP) :=
   #[global] knownr_make_and :: MakeAnd P Q PQ.
-Global Arguments KnownRMakeAnd {_} _%I _%I _%I.
+Global Arguments KnownRMakeAnd {_} _%_I _%_I _%_I.
 Global Hint Mode KnownRMakeAnd + - ! - : typeclass_instances.
 
 Class MakeOr {PROP : bi} (P Q PQ : PROP) := make_or_l : P ∨ Q ⊣⊢ PQ.
-Global Arguments MakeOr {_} _%I _%I _%I.
+Global Arguments MakeOr {_} _%_I _%_I _%_I.
 Global Hint Mode MakeOr + - - - : typeclass_instances.
 Class KnownLMakeOr {PROP : bi} (P Q PQ : PROP) :=
   #[global] knownl_make_or :: MakeOr P Q PQ.
-Global Arguments KnownLMakeOr {_} _%I _%I _%I.
+Global Arguments KnownLMakeOr {_} _%_I _%_I _%_I.
 Global Hint Mode KnownLMakeOr + ! - - : typeclass_instances.
 Class KnownRMakeOr {PROP : bi} (P Q PQ : PROP) := #[global] knownr_make_or :: MakeOr P Q PQ.
-Global Arguments KnownRMakeOr {_} _%I _%I _%I.
+Global Arguments KnownRMakeOr {_} _%_I _%_I _%_I.
 Global Hint Mode KnownRMakeOr + - ! - : typeclass_instances.
 
 Class MakeAffinely {PROP : bi} (P Q : PROP) :=
   make_affinely : <affine> P ⊣⊢ Q.
-Global Arguments MakeAffinely {_} _%I _%I.
+Global Arguments MakeAffinely {_} _%_I _%_I.
 Global Hint Mode MakeAffinely + - - : typeclass_instances.
 Class KnownMakeAffinely {PROP : bi} (P Q : PROP) :=
   #[global] known_make_affinely :: MakeAffinely P Q.
-Global Arguments KnownMakeAffinely {_} _%I _%I.
+Global Arguments KnownMakeAffinely {_} _%_I _%_I.
 Global Hint Mode KnownMakeAffinely + ! - : typeclass_instances.
 
 Class MakeIntuitionistically {PROP : bi} (P Q : PROP) :=
   make_intuitionistically : □ P ⊣⊢ Q.
-Global Arguments MakeIntuitionistically {_} _%I _%I.
+Global Arguments MakeIntuitionistically {_} _%_I _%_I.
 Global Hint Mode MakeIntuitionistically + - - : typeclass_instances.
 Class KnownMakeIntuitionistically {PROP : bi} (P Q : PROP) :=
   #[global] known_make_intuitionistically :: MakeIntuitionistically P Q.
-Global Arguments KnownMakeIntuitionistically {_} _%I _%I.
+Global Arguments KnownMakeIntuitionistically {_} _%_I _%_I.
 Global Hint Mode KnownMakeIntuitionistically + ! - : typeclass_instances.
 
 Class MakeAbsorbingly {PROP : bi} (P Q : PROP) :=
   make_absorbingly : <absorb> P ⊣⊢ Q.
-Global Arguments MakeAbsorbingly {_} _%I _%I.
+Global Arguments MakeAbsorbingly {_} _%_I _%_I.
 Global Hint Mode MakeAbsorbingly + - - : typeclass_instances.
 Class KnownMakeAbsorbingly {PROP : bi} (P Q : PROP) :=
   #[global] known_make_absorbingly :: MakeAbsorbingly P Q.
-Global Arguments KnownMakeAbsorbingly {_} _%I _%I.
+Global Arguments KnownMakeAbsorbingly {_} _%_I _%_I.
 Global Hint Mode KnownMakeAbsorbingly + ! - : typeclass_instances.
 
 Class MakePersistently {PROP : bi} (P Q : PROP) :=
   make_persistently : <pers> P ⊣⊢ Q.
-Global Arguments MakePersistently {_} _%I _%I.
+Global Arguments MakePersistently {_} _%_I _%_I.
 Global Hint Mode MakePersistently + - - : typeclass_instances.
 Class KnownMakePersistently {PROP : bi} (P Q : PROP) :=
   #[global] known_make_persistently :: MakePersistently P Q.
-Global Arguments KnownMakePersistently {_} _%I _%I.
+Global Arguments KnownMakePersistently {_} _%_I _%_I.
 Global Hint Mode KnownMakePersistently + ! - : typeclass_instances.
 
 Class MakeLaterN {PROP : bi} (n : nat) (P lP : PROP) :=
   make_laterN : ▷^n P ⊣⊢ lP.
-Global Arguments MakeLaterN {_} _%nat _%I _%I.
+Global Arguments MakeLaterN {_} _%_nat _%_I _%_I.
 Global Hint Mode MakeLaterN + + - - : typeclass_instances.
 Class KnownMakeLaterN {PROP : bi} (n : nat) (P lP : PROP) :=
   #[global] known_make_laterN :: MakeLaterN n P lP.
-Global Arguments KnownMakeLaterN {_} _%nat _%I _%I.
+Global Arguments KnownMakeLaterN {_} _%_nat _%_I _%_I.
 Global Hint Mode KnownMakeLaterN + + ! - : typeclass_instances.
 
 Class MakeExcept0 {PROP : bi} (P Q : PROP) :=
   make_except_0 : ◇ P ⊣⊢ Q.
-Global Arguments MakeExcept0 {_} _%I _%I.
+Global Arguments MakeExcept0 {_} _%_I _%_I.
 Global Hint Mode MakeExcept0 + - - : typeclass_instances.
 Class KnownMakeExcept0 {PROP : bi} (P Q : PROP) :=
   #[global] known_make_except_0 :: MakeExcept0 P Q.
-Global Arguments KnownMakeExcept0 {_} _%I _%I.
+Global Arguments KnownMakeExcept0 {_} _%_I _%_I.
 Global Hint Mode KnownMakeExcept0 + ! - : typeclass_instances.
diff --git a/iris/proofmode/coq_tactics.v b/iris/proofmode/coq_tactics.v
index 7e6dcdf808837a12ae6b0c3e767c608bb0befcca..24027fa80943def5bb4aaa99b5698ca86328b630 100644
--- a/iris/proofmode/coq_tactics.v
+++ b/iris/proofmode/coq_tactics.v
@@ -654,9 +654,9 @@ Class CombineSepsAsGives {PROP : bi} (Ps : list PROP) (Q R : PROP) := {
   combine_seps_as_gives_gives : [∗] Ps ⊢ <pers> R;
 }.
 Global Hint Mode CombineSepsAsGives + ! - - : typeclass_instances.
-Global Arguments CombineSepsAsGives {_} _%I _%I _%I.
-Global Arguments combine_seps_as_gives_as {_} _%I _%I _%I {_}.
-Global Arguments combine_seps_as_gives_gives {_} _%I _%I _%I {_}.
+Global Arguments CombineSepsAsGives {_} _%_I _%_I _%_I.
+Global Arguments combine_seps_as_gives_as {_} _%_I _%_I _%_I {_}.
+Global Arguments combine_seps_as_gives_gives {_} _%_I _%_I _%_I {_}.
 
 Global Instance combine_seps_as_gives_nil : @CombineSepsAsGives PROP [] emp True.
 Proof.
@@ -703,8 +703,8 @@ the following [CombineSepsAs] typeclass. *)
 Class CombineSepsAs {PROP : bi} (Ps : list PROP) (Q : PROP) :=
   combine_seps_as : [∗] Ps ⊢ Q.
 Global Hint Mode CombineSepsAs + ! - : typeclass_instances.
-Global Arguments CombineSepsAs {_} _%I _%I.
-Global Arguments combine_seps_as {_} _%I _%I {_}.
+Global Arguments CombineSepsAs {_} _%_I _%_I.
+Global Arguments combine_seps_as {_} _%_I _%_I {_}.
 
 (** To ensure consistency of the output [Q] with that of [CombineSepsAsGives],
 the only instance of [CombineSepsAs] is constructed with an instance of
diff --git a/iris/proofmode/environments.v b/iris/proofmode/environments.v
index 46a92dbdc1785fafe7e7e1ce1941ad9855ffb930..d8826235c36c7bde3cf3039d6cbbb9ab67c98293 100644
--- a/iris/proofmode/environments.v
+++ b/iris/proofmode/environments.v
@@ -271,7 +271,7 @@ Definition envs_entails {PROP : bi} (Δ : envs PROP) (Q : PROP) : Prop :=
 Definition envs_entails_unseal :
   @envs_entails = λ PROP (Δ : envs PROP) Q, (of_envs Δ ⊢ Q).
 Proof. by rewrite /envs_entails pre_envs_entails_unseal. Qed.
-Global Arguments envs_entails {PROP} Δ Q%I.
+Global Arguments envs_entails {PROP} Δ Q%_I.
 Global Instance: Params (@envs_entails) 1 := {}.
 
 Record envs_Forall2 {PROP : bi} (R : relation PROP) (Δ1 Δ2 : envs PROP) := {
diff --git a/iris/proofmode/monpred.v b/iris/proofmode/monpred.v
index 8f61cdb17c5e6b949fb4b1efb797eff61bf27ce2..7eebaed92ddd200650d4177ea93cfd82068d13ad 100644
--- a/iris/proofmode/monpred.v
+++ b/iris/proofmode/monpred.v
@@ -6,7 +6,7 @@ From iris.prelude Require Import options.
 Class MakeMonPredAt {I : biIndex} {PROP : bi} (i : I)
       (P : monPred I PROP) (𝓟 : PROP) :=
   make_monPred_at : P i ⊣⊢ 𝓟.
-Global Arguments MakeMonPredAt {_ _} _ _%I _%I.
+Global Arguments MakeMonPredAt {_ _} _ _%_I _%_I.
 (** Since [MakeMonPredAt] is used by [AsEmpValid] to import lemmas into the
 proof mode, the index [I] and BI [PROP] often contain evars. Hence, it is
 important to use the mode [!] also for the first two arguments. *)
@@ -24,7 +24,7 @@ Global Hint Extern 1 (IsBiIndexRel _ _) => unfold IsBiIndexRel; assumption
 Class FrameMonPredAt {I : biIndex} {PROP : bi} (p : bool) (i : I)
       (𝓡 : PROP) (P : monPred I PROP) (𝓠 : PROP) :=
   frame_monPred_at : □?p 𝓡 ∗ 𝓠 ⊢ P i.
-Global Arguments FrameMonPredAt {_ _} _ _ _%I _%I _%I.
+Global Arguments FrameMonPredAt {_ _} _ _ _%_I _%_I _%_I.
 Global Hint Mode FrameMonPredAt + + + - ! ! - : typeclass_instances.
 
 Section modalities.
diff --git a/iris/proofmode/notation.v b/iris/proofmode/notation.v
index da7af97dff01813d335e5a22778389a7c9a6b771..2e19926b3d782dbefb9bcf60a511c3f23106baa9 100644
--- a/iris/proofmode/notation.v
+++ b/iris/proofmode/notation.v
@@ -4,9 +4,9 @@ From iris.prelude Require Import options.
 
 Declare Scope proof_scope.
 Delimit Scope proof_scope with env.
-Global Arguments Envs _ _%proof_scope _%proof_scope _.
+Global Arguments Envs _ _%_proof_scope _%_proof_scope _.
 Global Arguments Enil {_}.
-Global Arguments Esnoc {_} _%proof_scope _%string _%I.
+Global Arguments Esnoc {_} _%_proof_scope _%_string _%_I.
 
 Notation "" := Enil (only printing) : proof_scope.
 Notation "Γ H : P" := (Esnoc Γ (INamed H) P%I)
diff --git a/iris_deprecated/base_logic/viewshifts.v b/iris_deprecated/base_logic/viewshifts.v
index 379bf4265e7a3cbd0e23a4372e40d29e2e9aa750..41dc61d3b1e2936aa5f77408fa20bb08e40ba892 100644
--- a/iris_deprecated/base_logic/viewshifts.v
+++ b/iris_deprecated/base_logic/viewshifts.v
@@ -11,7 +11,7 @@ From iris.prelude Require Import options.
 
 Definition vs `{!invGS Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
   □ (P -∗ |={E1,E2}=> Q).
-Global Arguments vs {_ _} _ _ _%I _%I.
+Global Arguments vs {_ _} _ _ _%_I _%_I.
 
 Global Instance: Params (@vs) 4 := {}.
 Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P Q)