diff --git a/iris/base_logic/algebra.v b/iris/base_logic/algebra.v
index ab1bea0d81f358d182794de2d0fc75e4f247e4dd..a86c5aedaab45476f12e5d14c3a9fe88c4f89224 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.
diff --git a/iris/base_logic/bi.v b/iris/base_logic/bi.v
index 77be327e62d43d67c5125e9e81b8c4830b5f6489..a16db04da4eb1dde3c3745937fa2b0683cef545d 100644
--- a/iris/base_logic/bi.v
+++ b/iris/base_logic/bi.v
@@ -176,7 +176,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).
 
 Global Instance ownM_ne : NonExpansive (@uPred_ownM M) := uPred_primitive.ownM_ne.
diff --git a/iris/base_logic/derived.v b/iris/base_logic/derived.v
index b81a3b475cbae9e93dc284185e08de8ed86cbb39..0dbfae8d2b9bcc50776045ef72faa2e736771c62 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 *)
diff --git a/iris/base_logic/upred.v b/iris/base_logic/upred.v
index a369af8d7e573341cf9ddc527b6bed7cabbd131e..d2b54213a97eeb5a64c4312515d0c7780dbc13b0 100644
--- a/iris/base_logic/upred.v
+++ b/iris/base_logic/upred.v
@@ -115,7 +115,7 @@ Record uPred (M : ucmra) : Type := UPred {
 this way. *)
 Local Coercion uPred_holds : uPred >-> Funclass.
 Bind Scope bi_scope with uPred.
-Global Arguments uPred_holds {_} _%I _ _ : simpl never.
+Global Arguments uPred_holds {_} _ _ _ : simpl never.
 Add Printing Constructor uPred.
 Global Instance: Params (@uPred_holds) 3 := {}.
 
diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index b2c883411a41b6878fc1c06573aa7d0db9d47c35..37618475395e2168d43afa59f42b2718d85fc8d8 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -6,6 +6,12 @@ From iris.prelude Require Import options.
 Import interface.bi derived_laws.bi derived_laws_later.bi.
 
 (** Notations for unary variants *)
+(* Change the scope locally, to have it inherited globally by the notations. *)
+Local Arguments big_opL {M} o {_ A} _%I !_ /.
+Local Arguments big_opS {M} o {_ A _ _} _%I _.
+Local Arguments big_opM {M} o {_ K _ _ A} _%I _.
+Local Arguments big_opMS {M} o {_ A _ _} _%I _.
+
 Notation "'[∗' 'list]' k ↦ x ∈ l , P" :=
   (big_opL bi_sep (λ k x, P) l) : bi_scope.
 Notation "'[∗' 'list]' x ∈ l , P" :=
@@ -44,7 +50,7 @@ Fixpoint big_sepL2 {PROP : bi} {A B}
   | _, _ => False
   end%I.
 Global Instance: Params (@big_sepL2) 3 := {}.
-Global Arguments big_sepL2 {PROP A B} _ !_ !_ /.
+Global Arguments big_sepL2 {PROP} {A B}%type_scope _%I (!_ !_)%list_scope /.
 Typeclasses Opaque big_sepL2.
 Notation "'[∗' 'list]' k ↦ x1 ; x2 ∈ l1 ; l2 , P" :=
   (big_sepL2 (λ k x1 x2, P) l1 l2) : bi_scope.
@@ -57,7 +63,7 @@ Definition big_sepM2_def {PROP : bi} `{Countable K} {A B}
    [∗ map] k ↦ xy ∈ map_zip m1 m2, Φ k xy.1 xy.2)%I.
 Definition big_sepM2_aux : seal (@big_sepM2_def). Proof. by eexists. Qed.
 Definition big_sepM2 := big_sepM2_aux.(unseal).
-Global Arguments big_sepM2 {PROP K _ _ A B} _ _ _.
+Global Arguments big_sepM2 {PROP} {K}%type_scope {_ _} {A B}%type_scope _%I _ _.
 Definition big_sepM2_eq : @big_sepM2 = _ := big_sepM2_aux.(seal_eq).
 Global Instance: Params (@big_sepM2) 6 := {}.
 Notation "'[∗' 'map]' k ↦ x1 ; x2 ∈ m1 ; m2 , P" :=
diff --git a/iris/bi/interface.v b/iris/bi/interface.v
index 5447c68eda4f7a0b43edd8fe4fc15f1f03a6074b..b7cd208de8b0ec57bd25bae074d6432b0c3c9543 100644
--- a/iris/bi/interface.v
+++ b/iris/bi/interface.v
@@ -182,6 +182,7 @@ Structure bi := Bi {
   bi_bi_later_mixin : BiLaterMixin bi_entails bi_pure bi_or bi_impl
                                    bi_forall bi_exist bi_sep bi_persistently bi_later;
 }.
+Bind Scope bi_scope with bi_car.
 
 Coercion bi_ofeO (PROP : bi) : ofe := Ofe PROP (bi_ofe_mixin PROP).
 Canonical Structure bi_ofeO.
@@ -204,25 +205,25 @@ Global Instance: Params (@bi_later) 1  := {}.
 Global Arguments bi_car : simpl never.
 Global Arguments bi_dist : simpl never.
 Global Arguments bi_equiv : simpl never.
-Global Arguments bi_entails {PROP} _%I _%I : simpl never, rename.
+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_and {PROP} _%I _%I : simpl never, rename.
-Global Arguments bi_or {PROP} _%I _%I : simpl never, rename.
-Global Arguments bi_impl {PROP} _%I _%I : 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_sep {PROP} _%I _%I : simpl never, rename.
-Global Arguments bi_wand {PROP} _%I _%I : simpl never, rename.
-Global Arguments bi_persistently {PROP} _%I : simpl never, rename.
-Global Arguments bi_later {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.
+Global Arguments bi_later {PROP} _ : simpl never, rename.
 
 Global Hint Extern 0 (bi_entails _ _) => reflexivity : core.
 Global Instance bi_rewrite_relation (PROP : bi) : RewriteRelation (@bi_entails PROP) := {}.
 Global Instance bi_inhabited {PROP : bi} : Inhabited PROP := populate (bi_pure True).
 
-Notation "P ⊢ Q" := (bi_entails P%I Q%I) : stdpp_scope.
-Notation "P '⊢@{' PROP } Q" := (bi_entails (PROP:=PROP) P%I Q%I) (only parsing) : stdpp_scope.
+Notation "P ⊢ Q" := (bi_entails P Q) : stdpp_scope.
+Notation "P '⊢@{' PROP } Q" := (bi_entails (PROP:=PROP) P Q) (only parsing) : stdpp_scope.
 Notation "(⊢)" := bi_entails (only parsing) : stdpp_scope.
 Notation "'(⊢@{' PROP } )" := (bi_entails (PROP:=PROP)) (only parsing) : stdpp_scope.
 
diff --git a/iris/bi/weakestpre.v b/iris/bi/weakestpre.v
index 3bcc9cfe9dcc497299278dab3522443882ee6984..b2d99f698a880df68289f193375be3a55e811c3b 100644
--- a/iris/bi/weakestpre.v
+++ b/iris/bi/weakestpre.v
@@ -41,15 +41,15 @@ Global Instance: Params (@twp) 7 := {}.
 (** Notations for partial weakest preconditions *)
 (** Notations without binder -- only parsing because they overlap with the
 notations with binder. *)
-Notation "'WP' e @ s ; E {{ Φ } }" := (wp s E e%E Φ)
+Notation "'WP' e @ s ; E {{ Φ } }" := (wp s E e Φ)
   (at level 20, e, Φ at level 200, only parsing) : bi_scope.
-Notation "'WP' e @ E {{ Φ } }" := (wp NotStuck E e%E Φ)
+Notation "'WP' e @ E {{ Φ } }" := (wp NotStuck E e Φ)
   (at level 20, e, Φ at level 200, only parsing) : bi_scope.
-Notation "'WP' e @ E ? {{ Φ } }" := (wp MaybeStuck E e%E Φ)
+Notation "'WP' e @ E ? {{ Φ } }" := (wp MaybeStuck E e Φ)
   (at level 20, e, Φ at level 200, only parsing) : bi_scope.
-Notation "'WP' e {{ Φ } }" := (wp NotStuck ⊤ e%E Φ)
+Notation "'WP' e {{ Φ } }" := (wp NotStuck ⊤ e Φ)
   (at level 20, e, Φ at level 200, only parsing) : bi_scope.
-Notation "'WP' e ? {{ Φ } }" := (wp MaybeStuck ⊤ e%E Φ)
+Notation "'WP' e ? {{ Φ } }" := (wp MaybeStuck ⊤ e Φ)
   (at level 20, e, Φ at level 200, only parsing) : bi_scope.
 
 (** Notations with binder.  The indentation for the inner format block is chosen