diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 8c1b1633301d80122cf5eb8e9333d929c6e37648..27a8999cd770544963b56e6489de921e1aacabfd 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -36,7 +36,7 @@ Notation "'[∗' 'mset]' x ∈ X , P" := (big_opMS bi_sep (λ x, P) X) : bi_scop
 version also ensures that both lists have the same length. Although this version
 can be defined in terms of the unary using a [zip] (see [big_sepL2_alt]), we do
 not define it that way to get better computational behavior (for [simpl]). *)
-Fixpoint big_sepL2 {SI} {PROP : bi SI} {A B}
+Fixpoint big_sepL2 `{SI: indexT} {PROP : bi} {A B}
     (Φ : nat → A → B → PROP) (l1 : list A) (l2 : list B) : PROP :=
   match l1, l2 with
   | [], [] => emp
@@ -45,13 +45,13 @@ Fixpoint big_sepL2 {SI} {PROP : bi SI} {A B}
   end%I.
 Global Instance: Params (@big_sepL2) 4 := {}.
 Global Arguments big_sepL2 {SI PROP A B} _ !_ !_ /.
-Typeclasses Opaque big_sepL2.
+Global Typeclasses Opaque big_sepL2.
 Notation "'[∗' 'list]' k ↦ x1 ; x2 ∈ l1 ; l2 , P" :=
   (big_sepL2 (λ k x1 x2, P) l1 l2) : bi_scope.
 Notation "'[∗' 'list]' x1 ; x2 ∈ l1 ; l2 , P" :=
   (big_sepL2 (λ _ x1 x2, P) l1 l2) : bi_scope.
 
-Definition big_sepM2_def {SI} {PROP : bi SI} `{Countable K} {A B}
+Definition big_sepM2_def `{SI: indexT} {PROP : bi} `{Countable K} {A B}
     (Φ : K → A → B → PROP) (m1 : gmap K A) (m2 : gmap K B) : PROP :=
   (⌜ ∀ k, is_Some (m1 !! k) ↔ is_Some (m2 !! k) ⌝ ∧
    [∗ map] k ↦ xy ∈ map_zip m1 m2, Φ k xy.1 xy.2)%I.
@@ -67,7 +67,7 @@ Notation "'[∗' 'map]' x1 ; x2 ∈ m1 ; m2 , P" :=
 
 (** * Properties *)
 Section big_op.
-Context {SI} {PROP : bi SI}.
+Context `{SI: indexT} {PROP : bi}.
 Implicit Types P Q : PROP.
 Implicit Types Ps Qs : list PROP.
 Implicit Types A : Type.
@@ -511,7 +511,7 @@ Section sep_list2.
     ([∗ list] k ↦ y1;y2 ∈ l1;l2, Φ k y1 y2) ⊣⊢ [∗ list] k ↦ y1;y2 ∈ l1';l2', Ψ k y1 y2.
   Proof.
     intros Hl1 Hl2 Hf. rewrite !big_sepL2_alt. f_equiv.
-    { unshelve f_equiv; first apply SI. f_equiv; by apply length_proper. }
+    { do 2 f_equiv; by apply length_proper. }
     apply big_opL_proper_2; [by f_equiv|].
     intros k [x1 y1] [x2 y2] (?&?&[=<- <-]&?&?)%lookup_zip_with_Some
       (?&?&[=<- <-]&?&?)%lookup_zip_with_Some [??]; naive_solver.
@@ -791,7 +791,7 @@ Proof.
   rewrite zip_diag big_sepL_fmap /=. done.
 Qed.
 
-Lemma big_sepL2_ne_2 {A B : ofe SI}
+Lemma big_sepL2_ne_2 {A B : ofe}
     (Φ Ψ : nat → A → B → PROP) l1 l2 l1' l2' n :
   l1 ≡{n}≡ l1' → l2 ≡{n}≡ l2' →
   (∀ k y1 y1' y2 y2',
@@ -1386,8 +1386,8 @@ Section map2.
       Φ k y1 y2 ⊣⊢ Ψ k y1' y2') →
     ([∗ map] k ↦ y1;y2 ∈ m1;m2, Φ k y1 y2) ⊣⊢ [∗ map] k ↦ y1;y2 ∈ m1';m2', Ψ k y1 y2.
   Proof.
-    intros Hm1 Hm2 Hf. rewrite big_sepM2_eq /big_sepM2_def. f_equiv.
-    { unshelve f_equiv; first apply SI; split; intros Hm k.
+    intros Hm1 Hm2 Hf. rewrite !big_sepM2_alt. f_equiv.
+    { f_equiv; split; intros Hm k.
       - trans (is_Some (m1 !! k)); [symmetry; apply is_Some_proper; by f_equiv|].
         rewrite Hm. apply is_Some_proper; by f_equiv.
       - trans (is_Some (m1' !! k)); [apply is_Some_proper; by f_equiv|].
@@ -1763,7 +1763,7 @@ Proof.
   rewrite map_zip_diag big_sepM_fmap. done.
 Qed.
 
-Lemma big_sepM2_ne_2 `{Countable K} (A B : ofe SI)
+Lemma big_sepM2_ne_2 `{Countable K} (A B : ofe)
     (Φ Ψ : K → A → B → PROP) m1 m2 m1' m2' n :
   m1 ≡{n}≡ m1' → m2 ≡{n}≡ m2' →
   (∀ k y1 y1' y2 y2',
diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v
index f6ade5f32389670b42d753966e3400295e974d23..3534ed8e6728761d4e820448ee3e1e07cd3d2692 100644
--- a/theories/bi/derived_connectives.v
+++ b/theories/bi/derived_connectives.v
@@ -1,89 +1,89 @@
 From iris.bi Require Export interface.
 From iris.algebra Require Import monoid.
 
-Definition bi_iff {SI} `{PROP : bi SI} (P Q : PROP) : PROP := ((P → Q) ∧ (Q → P))%I.
+Definition bi_iff `{SI: indexT} `{PROP : bi} (P Q : PROP) : PROP := ((P → Q) ∧ (Q → P))%I.
 Global Arguments bi_iff {_ _} _%I _%I : simpl never.
 Global Instance: Params (@bi_iff) 2 := {}.
 Infix "↔" := bi_iff : bi_scope.
 
-Definition bi_wand_iff {SI} `{PROP : bi SI} (P Q : PROP) : PROP :=
+Definition bi_wand_iff `{SI: indexT} `{PROP : bi} (P Q : PROP) : PROP :=
   ((P -∗ Q) ∧ (Q -∗ P))%I.
 Global Arguments bi_wand_iff {_ _} _%I _%I : simpl never.
 Global Instance: Params (@bi_wand_iff) 2 := {}.
 Infix "∗-∗" := bi_wand_iff : bi_scope.
 
-Class Persistent {SI} `{PROP : bi SI} (P : PROP) := persistent : P ⊢ <pers> P.
+Class Persistent `{SI: indexT} `{PROP : bi} (P : PROP) := persistent : P ⊢ <pers> P.
 Global Arguments Persistent {_ _} _%I : simpl never.
 Global Arguments persistent {_ _} _%I {_}.
 Global Hint Mode Persistent - + ! : typeclass_instances.
 Global Instance: Params (@Persistent) 2 := {}.
 
-Definition bi_affinely {SI} `{PROP : bi SI} (P : PROP) : PROP := (emp ∧ P)%I.
+Definition bi_affinely `{SI: indexT} `{PROP : bi} (P : PROP) : PROP := (emp ∧ P)%I.
 Global Arguments bi_affinely {_ _} _%I : simpl never.
 Global Instance: Params (@bi_affinely) 2 := {}.
-Typeclasses Opaque bi_affinely.
+Global Typeclasses Opaque bi_affinely.
 Notation "'<affine>' P" := (bi_affinely P) : bi_scope.
 
-Class Affine {SI} `{PROP : bi SI} (Q : PROP) := affine : Q ⊢ emp.
+Class Affine `{SI: indexT} `{PROP : bi} (Q : PROP) := affine : Q ⊢ emp.
 Global Arguments Affine {_ _} _%I : simpl never.
 Global Arguments affine {_ _} _%I {_}.
 Global Hint Mode Affine - + ! : typeclass_instances.
 
-Class BiAffine {SI} `(PROP : bi SI) := absorbing_bi (Q : PROP) : Affine Q.
+Class BiAffine `{SI: indexT} `(PROP : bi) := absorbing_bi (Q : PROP) : Affine Q.
 Global Hint Mode BiAffine - ! : typeclass_instances.
-Existing Instance absorbing_bi | 0.
+Global Existing Instance absorbing_bi | 0.
 
-Class BiPositive {SI} `(PROP : bi SI) :=
+Class BiPositive `{SI: indexT} `(PROP : bi) :=
   bi_positive (P Q : PROP) : <affine> (P ∗ Q) ⊢ <affine> P ∗ Q.
 Global Hint Mode BiPositive - ! : typeclass_instances.
 
-Definition bi_absorbingly {SI} `{PROP : bi SI} (P : PROP) : PROP := (True ∗ P)%I.
+Definition bi_absorbingly `{SI: indexT} `{PROP : bi} (P : PROP) : PROP := (True ∗ P)%I.
 Global Arguments bi_absorbingly {_ _} _%I : simpl never.
 Global Instance: Params (@bi_absorbingly) 2 := {}.
-Typeclasses Opaque bi_absorbingly.
+Global Typeclasses Opaque bi_absorbingly.
 Notation "'<absorb>' P" := (bi_absorbingly P) : bi_scope.
 
-Class Absorbing {SI} `{PROP : bi SI} (P : PROP) := absorbing : <absorb> P ⊢ P.
+Class Absorbing `{SI: indexT} `{PROP : bi} (P : PROP) := absorbing : <absorb> P ⊢ P.
 Global Arguments Absorbing {_ _} _%I : simpl never.
 Global Arguments absorbing {_ _} _%I.
 Global Hint Mode Absorbing - + ! : typeclass_instances.
 
-Definition bi_persistently_if {SI} `{PROP : bi SI} (p : bool) (P : PROP) : PROP :=
+Definition bi_persistently_if `{SI: indexT} `{PROP : bi} (p : bool) (P : PROP) : PROP :=
   (if p then <pers> P else P)%I.
 Global Arguments bi_persistently_if {_ _} !_ _%I /.
 Global Instance: Params (@bi_persistently_if) 3 := {}.
-Typeclasses Opaque bi_persistently_if.
+Global Typeclasses Opaque bi_persistently_if.
 Notation "'<pers>?' p P" := (bi_persistently_if p P) : bi_scope.
 
-Definition bi_affinely_if {SI} `{PROP : bi SI} (p : bool) (P : PROP) : PROP :=
+Definition bi_affinely_if `{SI: indexT} `{PROP : bi} (p : bool) (P : PROP) : PROP :=
   (if p then <affine> P else P)%I.
 Global Arguments bi_affinely_if {_ _} !_ _%I /.
 Global Instance: Params (@bi_affinely_if) 3 := {}.
-Typeclasses Opaque bi_affinely_if.
+Global Typeclasses Opaque bi_affinely_if.
 Notation "'<affine>?' p P" := (bi_affinely_if p P) : bi_scope.
 
-Definition bi_absorbingly_if {SI} `{PROP : bi SI} (p : bool) (P : PROP) : PROP :=
+Definition bi_absorbingly_if `{SI: indexT} `{PROP : bi} (p : bool) (P : PROP) : PROP :=
   (if p then <absorb> P else P)%I.
 Global Arguments bi_absorbingly_if {_ _} !_ _%I /.
 Global Instance: Params (@bi_absorbingly_if) 3 := {}.
-Typeclasses Opaque bi_absorbingly_if.
+Global Typeclasses Opaque bi_absorbingly_if.
 Notation "'<absorb>?' p P" := (bi_absorbingly_if p P) : bi_scope.
 
-Definition bi_intuitionistically {SI} `{PROP : bi SI} (P : PROP) : PROP :=
+Definition bi_intuitionistically `{SI: indexT} `{PROP : bi} (P : PROP) : PROP :=
   (<affine> <pers> P)%I.
 Global Arguments bi_intuitionistically {_ _} _%I : simpl never.
 Global Instance: Params (@bi_intuitionistically) 2 := {}.
-Typeclasses Opaque bi_intuitionistically.
+Global Typeclasses Opaque bi_intuitionistically.
 Notation "â–¡ P" := (bi_intuitionistically P) : bi_scope.
 
-Definition bi_intuitionistically_if {SI} `{PROP : bi SI} (p : bool) (P : PROP) : PROP :=
+Definition bi_intuitionistically_if `{SI: indexT} `{PROP : bi} (p : bool) (P : PROP) : PROP :=
   (if p then â–¡ P else P)%I.
 Global Arguments bi_intuitionistically_if {_ _} !_ _%I /.
 Global Instance: Params (@bi_intuitionistically_if) 3 := {}.
-Typeclasses Opaque bi_intuitionistically_if.
+Global Typeclasses Opaque bi_intuitionistically_if.
 Notation "'â–¡?' p P" := (bi_intuitionistically_if p P) : bi_scope.
 
-Fixpoint bi_laterN {SI} {PROP : bi SI} (n : nat) (P : PROP) : PROP :=
+Fixpoint bi_laterN `{SI: indexT} {PROP : bi} (n : nat) (P : PROP) : PROP :=
   match n with
   | O => P
   | S n' => â–· â–·^n' P
@@ -93,13 +93,13 @@ Global Arguments bi_laterN {_ _} !_%nat_scope _%I.
 Global Instance: Params (@bi_laterN) 3 := {}.
 Notation "â–·? p P" := (bi_laterN (Nat.b2n p) P) : bi_scope.
 
-Definition bi_except_0 {SI} `{PROP : bi SI} (P : PROP) : PROP := (▷ False ∨ P)%I.
+Definition bi_except_0 `{SI: indexT} `{PROP : bi} (P : PROP) : PROP := (▷ False ∨ P)%I.
 Global Arguments bi_except_0 {_ _} _%I : simpl never.
 Notation "â—‡ P" := (bi_except_0 P) : bi_scope.
 Global Instance: Params (@bi_except_0) 2 := {}.
-Typeclasses Opaque bi_except_0.
+Global Typeclasses Opaque bi_except_0.
 
-Class Timeless `{PROP : bi SI} (P : PROP) := timeless : ▷ P ⊢ ◇ P.
+Class Timeless `{SI: indexT} `{PROP : bi} (P : PROP) := timeless : ▷ P ⊢ ◇ P.
 Global Arguments Timeless {_ _} _%I : simpl never.
 Global Arguments timeless {_ _} _%I {_}.
 Global Hint Mode Timeless - + ! : typeclass_instances.
@@ -108,7 +108,7 @@ Global Instance: Params (@Timeless) 2 := {}.
 (** An optional precondition [mP] to [Q].
     TODO: We may actually consider generalizing this to a list of preconditions,
     and e.g. also using it for texan triples. *)
-Definition bi_wandM `{PROP : bi SI} (mP : option PROP) (Q : PROP) : PROP :=
+Definition bi_wandM `{SI: indexT} `{PROP : bi} (mP : option PROP) (Q : PROP) : PROP :=
   match mP with
   | None => Q
   | Some P => (P -∗ Q)%I
@@ -125,7 +125,7 @@ step-indexing of the logic in account.
 
 The internal/"strong" version of Löb [(▷ P → P) ⊢ P] is derivable from [BiLöb].
 It is provided by the lemma [löb] in [derived_laws_later]. *)
-Class BiLöb {SI} (PROP : bi SI) :=
+Class BiLöb `{SI: indexT} (PROP : bi) :=
   löb_weak (P : PROP) : (▷ P ⊢ P) → (True ⊢ P).
 Global Hint Mode BiLöb - ! : typeclass_instances.
 Global Arguments löb_weak {_ _ _} _ _.
@@ -139,25 +139,25 @@ described by this type class is derivable, so it is not included.
 
 An instance of [BiPureForall] itself is derivable if we assume excluded middle
 in Coq, see the lemma [bi_pure_forall_em] in [derived_laws]. *)
-Class BiPureForall {SI} (PROP : bi SI) :=
+Class BiPureForall `{SI: indexT} (PROP : bi) :=
   pure_forall_2 : ∀ {A} (φ : A → Prop), (∀ a, ⌜ φ a ⌝) ⊢@{PROP} ⌜ ∀ a, φ a ⌝.
 
 
 
-Class BiFinite {SI: indexT} (PROP: bi SI) := {
+Class BiFinite {SI: indexT} (PROP: bi) := {
   later_exist_false {A} (Φ : A → PROP) :
     (▷ ∃ a, Φ a) ⊢ ▷ False ∨ (∃ a, ▷ Φ a);
   later_sep_1 (P Q  : PROP): ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q;
 }.
 
 
-Class BiLaterOr {SI: indexT} (PROP: bi SI) := {
+Class BiLaterOr {SI: indexT} (PROP: bi) := {
   later_or_1 (P Q : PROP) :
     (▷ (P ∨ Q)) ⊢ (▷ P) ∨ (▷ Q);
 }.
 
 (* TODO: we make this a class for now, could be integrated with the normal BI interface *)
-Class BiTimeless {SI: indexT} (PROP: bi SI) := {
+Class BiTimeless {SI: indexT} (PROP: bi) := {
   pure_timeless φ:> Timeless (PROP:=PROP) ⌜φ⌝;
   later_sep_timeless (P Q: PROP): Timeless P → Timeless Q → ▷ (P ∗ Q) ⊢ (▷ P) ∗ (▷ Q);
   later_exist_timeless {X} (Ψ: X → PROP): (∀ x, Timeless (Ψ x)) → ▷ (∃ x: X, Ψ x) ⊢ ▷ False ∨ (∃ x: X, ▷ Ψ x);
diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index 255b4b1d892251185ab5bb88de82c3863fd58a19..88b78485150d8bbe7f039efd5b1007fbf889c099 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -15,7 +15,7 @@ Set Default Proof Using "Type*".
 Module bi.
 Import interface.bi.
 Section derived.
-Context {SI: indexT} {PROP : bi SI}.
+Context `{SI: indexT} {PROP : bi}.
 Implicit Types φ : Prop.
 Implicit Types P Q R : PROP.
 Implicit Types Ps : list PROP.
@@ -777,7 +777,7 @@ Proof.
 Qed.
 
 Section bi_affine.
-  Context `{BiAffine SI PROP}.
+  Context `{!BiAffine PROP}.
 
   Global Instance bi_affine_absorbing P : Absorbing P | 0.
   Proof. by rewrite /Absorbing /bi_absorbingly (affine True%I) left_id. Qed.
@@ -942,7 +942,7 @@ Proof.
 Qed.
 Lemma persistently_sep_2 P Q : <pers> P ∗ <pers> Q ⊢ <pers> (P ∗ Q).
 Proof. by rewrite -persistently_and_sep persistently_and -and_sep_persistently. Qed.
-Lemma persistently_sep `{BiPositive SI PROP} P Q : <pers> (P ∗ Q) ⊣⊢ <pers> P ∗ <pers> Q.
+Lemma persistently_sep `{!BiPositive PROP} P Q : <pers> (P ∗ Q) ⊣⊢ <pers> P ∗ <pers> Q.
 Proof.
   apply (anti_symm _); auto using persistently_sep_2.
   rewrite -persistently_affinely_elim affinely_sep -and_sep_persistently. apply and_intro.
@@ -984,7 +984,7 @@ Lemma impl_wand_persistently_2 P Q : (<pers> P -∗ Q) ⊢ (<pers> P → Q).
 Proof. apply impl_intro_l. by rewrite persistently_and_sep_l_1 wand_elim_r. Qed.
 
 Section persistently_affine_bi.
-  Context `{BiAffine SI PROP}.
+  Context `{!BiAffine PROP}.
 
   Lemma persistently_emp : <pers> emp ⊣⊢ emp.
   Proof. by rewrite -!True_emp persistently_pure. Qed.
@@ -1067,7 +1067,7 @@ Lemma intuitionistically_exist {A} (Φ : A → PROP) : □ (∃ x, Φ x) ⊣⊢
 Proof. by rewrite /bi_intuitionistically persistently_exist affinely_exist. Qed.
 Lemma intuitionistically_sep_2 P Q : □ P ∗ □ Q ⊢ □ (P ∗ Q).
 Proof. by rewrite /bi_intuitionistically affinely_sep_2 persistently_sep_2. Qed.
-Lemma intuitionistically_sep `{BiPositive SI PROP} P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q.
+Lemma intuitionistically_sep `{!BiPositive PROP} P Q : □ (P ∗ Q) ⊣⊢ □ P ∗ □ Q.
 Proof. by rewrite /bi_intuitionistically -affinely_sep -persistently_sep. Qed.
 
 Lemma intuitionistically_idemp P : □ □ P ⊣⊢ □ P.
@@ -1147,7 +1147,7 @@ Proof.
 Qed.
 
 Section bi_affine_intuitionistically.
-  Context `{BiAffine SI PROP}.
+  Context `{!BiAffine PROP}.
 
   Lemma intuitionistically_into_persistently P : □ P ⊣⊢ <pers> P.
   Proof. rewrite /bi_intuitionistically affine_affinely //. Qed.
@@ -1187,7 +1187,7 @@ Lemma affinely_if_exist {A} p (Ψ : A → PROP) :
 Proof. destruct p; simpl; auto using affinely_exist. Qed.
 Lemma affinely_if_sep_2 p P Q : <affine>?p P ∗ <affine>?p Q ⊢ <affine>?p (P ∗ Q).
 Proof. destruct p; simpl; auto using affinely_sep_2. Qed.
-Lemma affinely_if_sep `{BiPositive SI PROP} p P Q :
+Lemma affinely_if_sep `{!BiPositive PROP} p P Q :
   <affine>?p (P ∗ Q) ⊣⊢ <affine>?p P ∗ <affine>?p Q.
 Proof. destruct p; simpl; auto using affinely_sep. Qed.
 
@@ -1279,7 +1279,7 @@ Lemma persistently_if_exist {A} p (Ψ : A → PROP) :
 Proof. destruct p; simpl; auto using persistently_exist. Qed.
 Lemma persistently_if_sep_2 p P Q : <pers>?p P ∗ <pers>?p Q ⊢ <pers>?p (P ∗ Q).
 Proof. destruct p; simpl; auto using persistently_sep_2. Qed.
-Lemma persistently_if_sep `{BiPositive SI PROP} p P Q :
+Lemma persistently_if_sep `{!BiPositive PROP} p P Q :
   <pers>?p (P ∗ Q) ⊣⊢ <pers>?p P ∗ <pers>?p Q.
 Proof. destruct p; simpl; auto using persistently_sep. Qed.
 
@@ -1325,7 +1325,7 @@ Lemma intuitionistically_if_exist {A} p (Ψ : A → PROP) :
 Proof. destruct p; simpl; auto using intuitionistically_exist. Qed.
 Lemma intuitionistically_if_sep_2 p P Q : □?p P ∗ □?p Q ⊢ □?p (P ∗ Q).
 Proof. destruct p; simpl; auto using intuitionistically_sep_2. Qed.
-Lemma intuitionistically_if_sep `{BiPositive SI PROP} p P Q :
+Lemma intuitionistically_if_sep `{!BiPositive PROP} p P Q :
   □?p (P ∗ Q) ⊣⊢ □?p P ∗ □?p Q.
 Proof. destruct p; simpl; auto using intuitionistically_sep. Qed.
 
@@ -1416,7 +1416,7 @@ Lemma impl_wand_2 P `{!Persistent P} Q : (P -∗ Q) ⊢ P → Q.
 Proof. apply impl_intro_l. by rewrite persistent_and_sep_1 wand_elim_r. Qed.
 
 Section persistent_bi_absorbing.
-  Context `{BiAffine SI PROP}.
+  Context `{!BiAffine PROP}.
 
   Lemma persistent_and_sep P Q `{HPQ : !TCOr (Persistent P) (Persistent Q)} :
     P ∧ Q ⊣⊢ P ∗ Q.
@@ -1571,11 +1571,11 @@ Proof.
   - apply persistently_pure.
 Qed.
 
-Global Instance bi_persistently_sep_weak_homomorphism `{BiPositive SI PROP} :
+Global Instance bi_persistently_sep_weak_homomorphism `{!BiPositive PROP} :
   WeakMonoidHomomorphism bi_sep bi_sep (≡) (@bi_persistently SI PROP).
 Proof. split; [by apply _ ..|]. apply persistently_sep. Qed.
 
-Global Instance bi_persistently_sep_homomorphism `{BiAffine SI PROP} :
+Global Instance bi_persistently_sep_homomorphism `{!BiAffine PROP} :
   MonoidHomomorphism bi_sep bi_sep (≡) (@bi_persistently SI PROP).
 Proof. split; [by apply _ ..|]. apply persistently_emp. Qed.
 
@@ -1588,20 +1588,20 @@ Global Instance bi_persistently_sep_entails_homomorphism :
 Proof. split; [by apply _ ..|]. simpl. apply persistently_emp_intro. Qed.
 
 (* Limits *)
-Lemma limit_preserving_entails {A : ofe SI} `{Cofe SI A} (Φ Ψ : A → PROP) :
+Lemma limit_preserving_entails {A : ofe} `{!Cofe A} (Φ Ψ : A → PROP) :
   NonExpansive Φ → NonExpansive Ψ → LimitPreserving (λ x, Φ x ⊢ Ψ x).
 Proof.
   intros HΦ HΨ c HC. apply entails_eq_True, equiv_dist=>n.
   rewrite conv_compl; eauto using chain_cauchy. apply equiv_dist, entails_eq_True. done.
 Qed.
-Lemma limit_preserving_equiv {A : ofe SI} `{Cofe SI A} (Φ Ψ : A → PROP) :
+Lemma limit_preserving_equiv {A : ofe} `{!Cofe A} (Φ Ψ : A → PROP) :
   NonExpansive Φ → NonExpansive Ψ → LimitPreserving (λ x, Φ x ⊣⊢ Ψ x).
 Proof.
   intros HΦ HΨ. eapply limit_preserving_ext.
   { intros x. symmetry; apply equiv_spec. }
   apply limit_preserving_and; by apply limit_preserving_entails.
 Qed.
-Global Instance limit_preserving_Persistent {A:ofe SI} `{Cofe SI A} (Φ : A → PROP) :
+Global Instance limit_preserving_Persistent {A: ofe} `{!Cofe A} (Φ : A → PROP) :
   NonExpansive Φ → LimitPreserving (λ x, Persistent (Φ x)).
 Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
 End derived.
diff --git a/theories/bi/derived_laws_later.v b/theories/bi/derived_laws_later.v
index 945d58152dffc2bed8dbed33f6867af2ee546ae5..0cd1586041e930cedf0831862367433c2001eaa6 100644
--- a/theories/bi/derived_laws_later.v
+++ b/theories/bi/derived_laws_later.v
@@ -6,7 +6,7 @@ Module bi.
 Import interface.bi.
 Import derived_laws.bi.
 Section later_derived.
-Context {SI: indexT} {PROP : bi SI}.
+Context `{SI: indexT} {PROP : bi}.
 Implicit Types φ : Prop.
 Implicit Types P Q R : PROP.
 Implicit Types Ps : list PROP.
@@ -251,7 +251,7 @@ Proof. by rewrite /bi_intuitionistically -laterN_persistently laterN_affinely_2.
 Lemma laterN_intuitionistically_if_2 n p P : □?p ▷^n P ⊢ ▷^n □?p P.
 Proof. destruct p; simpl; auto using laterN_intuitionistically_2. Qed.
 (* FIXME: transfinite BI interface needs to add BiAffine because we do not have the commuting rule. *)
-Lemma laterN_absorbingly `{BiAffine SI PROP} n P : ▷^n <absorb> P ⊣⊢ <absorb> ▷^n P.
+Lemma laterN_absorbingly `{!BiAffine PROP} n P : ▷^n <absorb> P ⊣⊢ <absorb> ▷^n P.
 Proof. induction n as [|n IH]; simpl; eauto. by rewrite IH later_absorbingly. Qed.
 
 Global Instance laterN_persistent n P : Persistent P → Persistent (▷^n P).
@@ -346,7 +346,7 @@ Qed.
 
 Global Instance except_0_persistent P : Persistent P → Persistent (◇ P).
 Proof. rewrite /bi_except_0; apply _. Qed.
-Global Instance except_0_absorbing `{BiAffine SI PROP} P : Absorbing P → Absorbing (◇ P).
+Global Instance except_0_absorbing `{!BiAffine PROP} P : Absorbing P → Absorbing (◇ P).
 Proof. rewrite /bi_except_0; apply _. Qed.
 
 (* Timeless instances *)
diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index 70dc66e88e28f1d5d654188d7fb9eac24bbec998..faf89a4cbe54af651d6549cb6229d86cd05a11c6 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -10,13 +10,13 @@ Class Embed (A B : Type) := embed : A → B.
 Global Arguments embed {_ _ _} _%I : simpl never.
 Notation "⎡ P ⎤" := (embed P) : bi_scope.
 Global Instance: Params (@embed) 3 := {}.
-Typeclasses Opaque embed.
+Global Typeclasses Opaque embed.
 
 Global Hint Mode Embed ! - : typeclass_instances.
 Global Hint Mode Embed - ! : typeclass_instances.
 
 (* Mixins allow us to create instances easily without having to use Program *)
-Record BiEmbedMixin {SI} (PROP1 PROP2 : bi SI) `(Embed PROP1 PROP2) := {
+Record BiEmbedMixin `{SI: indexT} (PROP1 PROP2 : bi) `(Embed PROP1 PROP2) := {
   bi_embed_mixin_ne : NonExpansive (embed (A:=PROP1) (B:=PROP2));
   bi_embed_mixin_mono : Proper ((⊢) ==> (⊢)) (embed (A:=PROP1) (B:=PROP2));
   bi_embed_mixin_emp_valid_inj (P : PROP1) :
@@ -26,7 +26,7 @@ Record BiEmbedMixin {SI} (PROP1 PROP2 : bi SI) `(Embed PROP1 PROP2) := {
   externally (i.e., as [Inj (dist n) (dist n) embed]), it is expressed using the
   internal equality of _any other_ BI [PROP']. This is more general, as we do
   not have any machinary to embed [siProp] into a BI with internal equality. *)
-  bi_embed_mixin_interal_inj {PROP': bi SI} `{!BiInternalEq PROP'} (P Q : PROP1) :
+  bi_embed_mixin_interal_inj {PROP': bi} `{!BiInternalEq PROP'} (P Q : PROP1) :
     ⎡P⎤ ≡ ⎡Q⎤ ⊢@{PROP'} (P ≡ Q);
   bi_embed_mixin_emp_2 : emp ⊢@{PROP2} ⎡emp⎤;
   bi_embed_mixin_impl_2 (P Q : PROP1) :
@@ -43,7 +43,7 @@ Record BiEmbedMixin {SI} (PROP1 PROP2 : bi SI) `(Embed PROP1 PROP2) := {
     ⎡<pers> P⎤ ⊣⊢@{PROP2} <pers> ⎡P⎤
 }.
 
-Class BiEmbed {SI} (PROP1 PROP2 : bi SI) := {
+Class BiEmbed `{SI: indexT} (PROP1 PROP2 : bi) := {
   bi_embed_embed :> Embed PROP1 PROP2;
   bi_embed_mixin : BiEmbedMixin PROP1 PROP2 bi_embed_embed;
 }.
@@ -51,42 +51,42 @@ Global Hint Mode BiEmbed - ! - : typeclass_instances.
 Global Hint Mode BiEmbed - - ! : typeclass_instances.
 Global Arguments bi_embed_embed : simpl never.
 
-Class BiEmbedEmp {SI} (PROP1 PROP2 : bi SI) `{BiEmbed SI PROP1 PROP2} :=
+Class BiEmbedEmp `{SI: indexT} (PROP1 PROP2 : bi) `{!BiEmbed PROP1 PROP2} :=
   embed_emp_1 : ⎡ emp : PROP1 ⎤ ⊢ emp.
 Global Hint Mode BiEmbedEmp - ! - - : typeclass_instances.
 Global Hint Mode BiEmbedEmp - - ! - : typeclass_instances.
 
-Class BiEmbedLater {SI} (PROP1 PROP2 : bi SI) `{!BiEmbed PROP1 PROP2} :=
+Class BiEmbedLater `{SI: indexT} (PROP1 PROP2 : bi) `{!BiEmbed PROP1 PROP2} :=
   embed_later P : ⎡▷ P⎤ ⊣⊢@{PROP2} ▷ ⎡P⎤.
 Global Hint Mode BiEmbedLater - ! - - : typeclass_instances.
 Global Hint Mode BiEmbedLater - - ! - : typeclass_instances.
 
-Class BiEmbedInternalEq {SI} (PROP1 PROP2 : bi SI)
+Class BiEmbedInternalEq `{SI: indexT} (PROP1 PROP2 : bi)
     `{!BiEmbed PROP1 PROP2, !BiInternalEq PROP1, !BiInternalEq PROP2} :=
-  embed_internal_eq_1 (A : ofe SI) (x y : A) : ⎡x ≡ y⎤ ⊢@{PROP2} x ≡ y.
+  embed_internal_eq_1 (A : ofe) (x y : A) : ⎡x ≡ y⎤ ⊢@{PROP2} x ≡ y.
 Global Hint Mode BiEmbedInternalEq - ! - - - - : typeclass_instances.
 Global Hint Mode BiEmbedInternalEq - - ! - - - : typeclass_instances.
 
-Class BiEmbedBUpd {SI} (PROP1 PROP2 : bi SI)
+Class BiEmbedBUpd `{SI: indexT} (PROP1 PROP2 : bi)
     `{!BiEmbed PROP1 PROP2, !BiBUpd PROP1, !BiBUpd PROP2} :=
   embed_bupd P : ⎡|==> P⎤ ⊣⊢@{PROP2} |==> ⎡P⎤.
 Global Hint Mode BiEmbedBUpd - - ! - - - : typeclass_instances.
 Global Hint Mode BiEmbedBUpd - ! - - - - : typeclass_instances.
 
-Class BiEmbedFUpd {SI} (PROP1 PROP2 : bi SI)
+Class BiEmbedFUpd `{SI: indexT} (PROP1 PROP2 : bi)
     `{!BiEmbed PROP1 PROP2, !BiFUpd PROP1, !BiFUpd PROP2} :=
   embed_fupd E1 E2 P : ⎡|={E1,E2}=> P⎤ ⊣⊢@{PROP2} |={E1,E2}=> ⎡P⎤.
 Global Hint Mode BiEmbedFUpd - - ! - - - : typeclass_instances.
 Global Hint Mode BiEmbedFUpd - ! - - - - : typeclass_instances.
 
-Class BiEmbedPlainly {SI} (PROP1 PROP2 : bi SI)
+Class BiEmbedPlainly `{SI: indexT} (PROP1 PROP2 : bi)
     `{!BiEmbed PROP1 PROP2, !BiPlainly PROP1, !BiPlainly PROP2} :=
   embed_plainly (P : PROP1) : ⎡■ P⎤ ⊣⊢@{PROP2} ■ ⎡P⎤.
 Global Hint Mode BiEmbedPlainly - - ! - - - : typeclass_instances.
 Global Hint Mode BiEmbedPlainly - ! - - - - : typeclass_instances.
 
 Section embed_laws.
-  Context {SI} {PROP1 PROP2: bi SI} `{!BiEmbed PROP1 PROP2}.
+  Context `{SI: indexT} {PROP1 PROP2: bi} `{!BiEmbed PROP1 PROP2}.
   Local Notation embed := (embed (A:=PROP1) (B:=PROP2)).
   Local Notation "⎡ P ⎤" := (embed P) : bi_scope.
   Implicit Types P : PROP1.
@@ -117,7 +117,7 @@ Section embed_laws.
 End embed_laws.
 
 Section embed.
-  Context {SI} {PROP1 PROP2: bi SI} `{!BiEmbed PROP1 PROP2}.
+  Context `{SI: indexT} {PROP1 PROP2: bi} `{!BiEmbed PROP1 PROP2}.
   Local Notation embed := (embed (A:=PROP1) (B:=PROP2)).
   Local Notation "⎡ P ⎤" := (embed P) : bi_scope.
   Implicit Types P Q R : PROP1.
@@ -291,7 +291,7 @@ Section embed.
   Section internal_eq.
     Context `{!BiInternalEq PROP1, !BiInternalEq PROP2, !BiEmbedInternalEq PROP1 PROP2}.
 
-    Lemma embed_internal_eq (A : ofe SI) (x y : A) : ⎡x ≡ y⎤ ⊣⊢@{PROP2} x ≡ y.
+    Lemma embed_internal_eq (A : ofe) (x y : A) : ⎡x ≡ y⎤ ⊣⊢@{PROP2} x ≡ y.
     Proof.
       apply bi.equiv_spec; split; [apply embed_internal_eq_1|].
       etrans; [apply (internal_eq_rewrite x y (λ y, ⎡x ≡ y⎤%I)); solve_proper|].
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index d3287b632a3d95b828037b24b8fcbf02eaa1ae64..024e77cd78928c0e63fa767e275570c5a7320c7b 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -4,7 +4,7 @@ From iris.prelude Require Import options.
 Set Primitive Projections.
 
 Section bi_mixin.
-  Context {SI: indexT} {PROP : Type} `{Dist SI PROP, Equiv PROP}.
+  Context `{SI: indexT} {PROP : Type} `{!Dist PROP, Equiv PROP}.
   Context (bi_entails : PROP → PROP → Prop).
   Context (bi_emp : PROP).
   Context (bi_pure : Prop → PROP).
@@ -153,9 +153,9 @@ Section bi_mixin.
   Qed.
 End bi_mixin.
 
-Structure bi {SI} := Bi {
+Structure bi `{SI: indexT} := Bi {
   bi_car :> Type;
-  bi_dist : Dist SI bi_car;
+  bi_dist : Dist bi_car;
   bi_equiv : Equiv bi_car;
   bi_entails : bi_car → bi_car → Prop;
   bi_emp : bi_car;
@@ -169,18 +169,17 @@ Structure bi {SI} := Bi {
   bi_wand : bi_car → bi_car → bi_car;
   bi_persistently : bi_car → bi_car;
   bi_later : bi_car → bi_car;
-  bi_ofe_mixin : OfeMixin SI bi_car;
+  bi_ofe_mixin : OfeMixin bi_car;
   bi_cofe : Cofe (Ofe bi_car bi_ofe_mixin);
   bi_bi_mixin : BiMixin bi_entails bi_emp bi_pure bi_and bi_or bi_impl bi_forall
                         bi_exist bi_sep bi_wand bi_persistently;
   bi_bi_later_mixin : BiLaterMixin bi_entails bi_pure bi_or bi_impl
                                    bi_forall bi_sep bi_persistently bi_later;
 }.
-Arguments bi _: clear implicits.
 
-Coercion bi_ofeO {SI: indexT} (PROP : bi SI) : ofe SI := Ofe PROP (bi_ofe_mixin PROP).
+Coercion bi_ofeO `{SI: indexT} (PROP : bi) : ofe := Ofe PROP (bi_ofe_mixin PROP).
 Canonical Structure bi_ofeO.
-Global Instance bi_cofe' {SI: indexT} (PROP : bi SI) : Cofe PROP.
+Global Instance bi_cofe' `{SI: indexT} (PROP : bi) : Cofe PROP.
 Proof. apply bi_cofe. Qed.
 
 Global Instance: Params (@bi_entails) 2 := {}.
@@ -213,8 +212,8 @@ Global Arguments bi_persistently {_ PROP} _%I : simpl never, rename.
 Global Arguments bi_later {_ PROP} _%I : simpl never, rename.
 
 Global Hint Extern 0 (bi_entails _ _) => reflexivity : core.
-Global Instance bi_rewrite_relation {SI: indexT} (PROP : bi SI) : RewriteRelation (@bi_entails SI PROP) := {}.
-Global Instance bi_inhabited {SI: indexT} {PROP : bi SI} : Inhabited PROP := populate (bi_pure True).
+Global Instance bi_rewrite_relation `{SI: indexT} (PROP : bi) : RewriteRelation (@bi_entails SI PROP) := {}.
+Global Instance bi_inhabited `{SI: indexT} {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.
@@ -251,10 +250,10 @@ Notation "'<pers>' P" := (bi_persistently P) : bi_scope.
 
 Notation "â–· P" := (bi_later P) : bi_scope.
 
-Definition bi_emp_valid {SI: indexT} {PROP : bi SI} (P : PROP) : Prop := (emp ⊢ P).
+Definition bi_emp_valid `{SI: indexT} {PROP : bi} (P : PROP) : Prop := (emp ⊢ P).
 
 Global Arguments bi_emp_valid {_ _} _%I : simpl never.
-Typeclasses Opaque bi_emp_valid.
+Global Typeclasses Opaque bi_emp_valid.
 
 Notation "⊢ Q" := (bi_emp_valid Q%I) : stdpp_scope.
 Notation "'⊢@{' PROP } Q" := (@bi_emp_valid _ PROP Q%I) (only parsing) : stdpp_scope.
@@ -265,7 +264,7 @@ Notation "( P ⊢.)" := (bi_entails P) (only parsing) : stdpp_scope.
 
 Module bi.
 Section bi_laws.
-Context {SI} {PROP : bi SI}.
+Context `{SI: indexT} {PROP : bi}.
 Implicit Types φ : Prop.
 Implicit Types P Q R : PROP.
 Implicit Types A : Type.
diff --git a/theories/bi/internal_eq.v b/theories/bi/internal_eq.v
index f4194726eedb844ed3da72c077297768fb965d83..0377ab52213cab16d572b298d131910b0137e0e0 100644
--- a/theories/bi/internal_eq.v
+++ b/theories/bi/internal_eq.v
@@ -6,8 +6,8 @@ Import interface.bi derived_laws.bi derived_laws_later.bi.
 Internal equality is not part of the [bi] canonical structure as [internal_eq]
 can only be given a definition that satisfies [NonExpansive2 internal_eq] _and_
 [▷ (x ≡ y) ⊢ Next x ≡ Next y] if the BI is step-indexed. *)
-Class InternalEq {SI} (PROP : bi SI) :=
-  internal_eq : ∀ {A : ofe SI}, A → A → PROP.
+Class InternalEq `{SI: indexT} (PROP : bi) :=
+  internal_eq : ∀ {A : ofe}, A → A → PROP.
 Global Arguments internal_eq {_ _ _ _} _ _ : simpl never.
 Global Hint Mode InternalEq - ! : typeclass_instances.
 Global Instance: Params (@internal_eq) 4 := {}.
@@ -19,24 +19,24 @@ Notation "(.≡ X )" := (λ Y, Y ≡ X)%I (only parsing) : bi_scope.
 Notation "(≡@{ A } )" := (internal_eq (A:=A)) (only parsing) : bi_scope.
 
 (* Mixins allow us to create instances easily without having to use Program *)
-Record BiInternalEqMixin {SI} (PROP : bi SI) `(!InternalEq PROP) := {
-  bi_internal_eq_mixin_internal_eq_ne (A : ofe SI) : NonExpansive2 (@internal_eq SI PROP _ A);
-  bi_internal_eq_mixin_internal_eq_refl {A : ofe SI} (P : PROP) (a : A) : P ⊢ a ≡ a;
-  bi_internal_eq_mixin_internal_eq_rewrite {A : ofe SI} a b (Ψ : A → PROP) :
+Record BiInternalEqMixin `{SI: indexT} (PROP : bi) `(!InternalEq PROP) := {
+  bi_internal_eq_mixin_internal_eq_ne (A : ofe) : NonExpansive2 (@internal_eq SI PROP _ A);
+  bi_internal_eq_mixin_internal_eq_refl {A : ofe} (P : PROP) (a : A) : P ⊢ a ≡ a;
+  bi_internal_eq_mixin_internal_eq_rewrite {A : ofe} a b (Ψ : A → PROP) :
     NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b;
-  bi_internal_eq_mixin_fun_extI {A} {B : A → ofe SI} (f g : discrete_fun B) :
+  bi_internal_eq_mixin_fun_extI {A} {B : A → ofe} (f g : discrete_fun B) :
     (∀ x, f x ≡ g x) ⊢@{PROP} f ≡ g;
-  bi_internal_eq_mixin_sig_equivI_1 {A : ofe SI} (P : A → Prop) (x y : sig P) :
+  bi_internal_eq_mixin_sig_equivI_1 {A : ofe} (P : A → Prop) (x y : sig P) :
     `x ≡ `y ⊢@{PROP} x ≡ y;
-  bi_internal_eq_mixin_discrete_eq_1 {A : ofe SI} (a b : A) :
+  bi_internal_eq_mixin_discrete_eq_1 {A : ofe} (a b : A) :
     Discrete a → a ≡ b ⊢@{PROP} ⌜a ≡ b⌝;
-  bi_internal_eq_mixin_later_equivI_1 {A : ofe SI} (x y : A) :
+  bi_internal_eq_mixin_later_equivI_1 {A : ofe} (x y : A) :
     Next x ≡ Next y ⊢@{PROP} ▷ (x ≡ y);
-  bi_internal_eq_mixin_later_equivI_2 {A : ofe SI} (x y : A) :
+  bi_internal_eq_mixin_later_equivI_2 {A : ofe} (x y : A) :
     ▷ (x ≡ y) ⊢@{PROP} Next x ≡ Next y;
 }.
 
-Class BiInternalEq {SI} (PROP : bi SI) := {
+Class BiInternalEq `{SI: indexT} (PROP : bi) := {
   bi_internal_eq_internal_eq :> InternalEq PROP;
   bi_internal_eq_mixin : BiInternalEqMixin PROP bi_internal_eq_internal_eq;
 }.
@@ -44,44 +44,44 @@ Global Hint Mode BiInternalEq - ! : typeclass_instances.
 Global Arguments bi_internal_eq_internal_eq : simpl never.
 
 Section internal_eq_laws.
-  Context {SI} {PROP: bi SI} `{!BiInternalEq PROP}.
+  Context `{SI: indexT} {PROP: bi} `{!BiInternalEq PROP}.
   Implicit Types P Q : PROP.
 
-  Global Instance internal_eq_ne (A : ofe SI) : NonExpansive2 (@internal_eq SI PROP _ A).
+  Global Instance internal_eq_ne (A : ofe) : NonExpansive2 (@internal_eq SI PROP _ A).
   Proof. eapply bi_internal_eq_mixin_internal_eq_ne, (bi_internal_eq_mixin). Qed.
 
-  Lemma internal_eq_refl {A : ofe SI} P (a : A) : P ⊢ a ≡ a.
+  Lemma internal_eq_refl {A : ofe} P (a : A) : P ⊢ a ≡ a.
   Proof. eapply bi_internal_eq_mixin_internal_eq_refl, bi_internal_eq_mixin. Qed.
-  Lemma internal_eq_rewrite {A : ofe SI} a b (Ψ : A → PROP) :
+  Lemma internal_eq_rewrite {A : ofe} a b (Ψ : A → PROP) :
     NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b.
   Proof. eapply bi_internal_eq_mixin_internal_eq_rewrite, bi_internal_eq_mixin. Qed.
 
-  Lemma fun_extI {A} {B : A → ofe SI} (f g : discrete_fun B) :
+  Lemma fun_extI {A} {B : A → ofe} (f g : discrete_fun B) :
     (∀ x, f x ≡ g x) ⊢@{PROP} f ≡ g.
   Proof. eapply bi_internal_eq_mixin_fun_extI, bi_internal_eq_mixin. Qed.
-  Lemma sig_equivI_1 {A : ofe SI} (P : A → Prop) (x y : sig P) :
+  Lemma sig_equivI_1 {A : ofe} (P : A → Prop) (x y : sig P) :
     `x ≡ `y ⊢@{PROP} x ≡ y.
   Proof. eapply bi_internal_eq_mixin_sig_equivI_1, bi_internal_eq_mixin. Qed.
-  Lemma discrete_eq_1 {A : ofe SI} (a b : A) :
+  Lemma discrete_eq_1 {A : ofe} (a b : A) :
     Discrete a → a ≡ b ⊢@{PROP} ⌜a ≡ b⌝.
   Proof. eapply bi_internal_eq_mixin_discrete_eq_1, bi_internal_eq_mixin. Qed.
 
-  Lemma later_equivI_1 {A : ofe SI} (x y : A) : Next x ≡ Next y ⊢@{PROP} ▷ (x ≡ y).
+  Lemma later_equivI_1 {A : ofe} (x y : A) : Next x ≡ Next y ⊢@{PROP} ▷ (x ≡ y).
   Proof. eapply bi_internal_eq_mixin_later_equivI_1, bi_internal_eq_mixin. Qed.
-  Lemma later_equivI_2 {A : ofe SI} (x y : A) : ▷ (x ≡ y) ⊢@{PROP} Next x ≡ Next y.
+  Lemma later_equivI_2 {A : ofe} (x y : A) : ▷ (x ≡ y) ⊢@{PROP} Next x ≡ Next y.
   Proof. eapply bi_internal_eq_mixin_later_equivI_2, bi_internal_eq_mixin. Qed.
 End internal_eq_laws.
 
 (* Derived laws *)
 Section internal_eq_derived.
-Context {SI} {PROP: bi SI} `{!BiInternalEq PROP}.
+Context `{SI: indexT} {PROP: bi} `{!BiInternalEq PROP}.
 Implicit Types P : PROP.
 
 (* Force implicit argument PROP *)
 Notation "P ⊢ Q" := (P ⊢@{PROP} Q).
 Notation "P ⊣⊢ Q" := (P ⊣⊢@{PROP} Q).
 
-Global Instance internal_eq_proper (A : ofe SI) :
+Global Instance internal_eq_proper (A : ofe) :
   Proper ((≡) ==> (≡) ==> (⊣⊢)) (@internal_eq SI PROP _ A) := ne_proper_2 _.
 
 (* Equality *)
@@ -90,31 +90,31 @@ Local Hint Resolve and_elim_l' and_elim_r' and_intro forall_intro : core.
 Local Hint Resolve internal_eq_refl : core.
 Local Hint Extern 100 (NonExpansive _) => solve_proper : core.
 
-Lemma equiv_internal_eq {A : ofe SI} P (a b : A) : a ≡ b → P ⊢ a ≡ b.
+Lemma equiv_internal_eq {A : ofe} P (a b : A) : a ≡ b → P ⊢ a ≡ b.
 Proof. intros ->. auto. Qed.
-Lemma internal_eq_rewrite' {A : ofe SI} a b (Ψ : A → PROP) P
+Lemma internal_eq_rewrite' {A : ofe} a b (Ψ : A → PROP) P
   {HΨ : NonExpansive Ψ} : (P ⊢ a ≡ b) → (P ⊢ Ψ a) → P ⊢ Ψ b.
 Proof.
   intros Heq HΨa. rewrite -(idemp bi_and P) {1}Heq HΨa.
   apply impl_elim_l'. by apply internal_eq_rewrite.
 Qed.
 
-Lemma internal_eq_sym {A : ofe SI} (a b : A) : a ≡ b ⊢ b ≡ a.
+Lemma internal_eq_sym {A : ofe} (a b : A) : a ≡ b ⊢ b ≡ a.
 Proof. apply (internal_eq_rewrite' a b (λ b, b ≡ a)%I); auto. Qed.
 Lemma internal_eq_iff P Q : P ≡ Q ⊢ P ↔ Q.
 Proof. apply (internal_eq_rewrite' P Q (λ Q, P ↔ Q))%I; auto using iff_refl. Qed.
 
-Lemma f_equivI {A B : ofe SI} (f : A → B) `{!NonExpansive f} x y :
+Lemma f_equivI {A B : ofe} (f : A → B) `{!NonExpansive f} x y :
   x ≡ y ⊢ f x ≡ f y.
 Proof. apply (internal_eq_rewrite' x y (λ y, f x ≡ f y)%I); auto. Qed.
-Lemma f_equivI_contractive {A B : ofe SI} (f : A → B) `{Hf : !Contractive f} x y :
+Lemma f_equivI_contractive {A B : ofe} (f : A → B) `{Hf : !Contractive f} x y :
   ▷ (x ≡ y) ⊢ f x ≡ f y.
 Proof.
   rewrite later_equivI_2. move: Hf=>/contractive_alt [g [? Hfg]]. rewrite !Hfg.
   by apply f_equivI.
 Qed.
 
-Lemma prod_equivI {A B : ofe SI} (x y : A * B) : x ≡ y ⊣⊢ x.1 ≡ y.1 ∧ x.2 ≡ y.2.
+Lemma prod_equivI {A B : ofe} (x y : A * B) : x ≡ y ⊣⊢ x.1 ≡ y.1 ∧ x.2 ≡ y.2.
 Proof.
   apply (anti_symm _).
   - apply and_intro; apply f_equivI; apply _.
@@ -122,7 +122,7 @@ Proof.
     apply (internal_eq_rewrite' (x.1) (y.1) (λ a, (x.1,x.2) ≡ (a,y.2))%I); auto.
     apply (internal_eq_rewrite' (x.2) (y.2) (λ b, (x.1,x.2) ≡ (x.1,b))%I); auto.
 Qed.
-Lemma sum_equivI {A B : ofe SI} (x y : A + B) :
+Lemma sum_equivI {A B : ofe} (x y : A + B) :
   x ≡ y ⊣⊢
     match x, y with
     | inl a, inl a' => a ≡ a' | inr b, inr b' => b ≡ b' | _, _ => False
@@ -136,7 +136,7 @@ Proof.
     destruct x; auto.
   - destruct x as [a|b], y as [a'|b']; auto; apply f_equivI, _.
 Qed.
-Lemma option_equivI {A : ofe SI} (x y : option A) :
+Lemma option_equivI {A : ofe} (x y : option A) :
   x ≡ y ⊣⊢ match x, y with
            | Some a, Some a' => a ≡ a' | None, None => True | _, _ => False
            end.
@@ -150,7 +150,7 @@ Proof.
   - destruct x as [a|], y as [a'|]; auto. apply f_equivI, _.
 Qed.
 
-Lemma sig_equivI {A : ofe SI} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊣⊢ x ≡ y.
+Lemma sig_equivI {A : ofe} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊣⊢ x ≡ y.
 Proof.
   apply (anti_symm _).
   - apply sig_equivI_1.
@@ -160,7 +160,7 @@ Qed.
 Section sigT_equivI.
 Import EqNotations.
 
-Lemma sigT_equivI {A : Type} {P : A → ofe SI} (x y : sigT P) :
+Lemma sigT_equivI {A : Type} {P : A → ofe} (x y : sigT P) :
   x ≡ y ⊣⊢
   ∃ eq : projT1 x = projT1 y, rew eq in projT2 x ≡ projT2 y.
 Proof.
@@ -176,12 +176,12 @@ Proof.
 Qed.
 End sigT_equivI.
 
-Lemma discrete_fun_equivI {A} {B : A → ofe SI} (f g : discrete_fun B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
+Lemma discrete_fun_equivI {A} {B : A → ofe} (f g : discrete_fun B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
 Proof.
   apply (anti_symm _); auto using fun_extI.
   apply (internal_eq_rewrite' f g (λ g, ∀ x : A, f x ≡ g x)%I); auto.
 Qed.
-Lemma ofe_morO_equivI {A B : ofe SI} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
+Lemma ofe_morO_equivI {A B : ofe} (f g : A -n> B) : f ≡ g ⊣⊢ ∀ x, f x ≡ g x.
 Proof.
   apply (anti_symm _).
   - apply (internal_eq_rewrite' f g (λ g, ∀ x : A, f x ≡ g x)%I); auto.
@@ -195,20 +195,20 @@ Proof.
     by rewrite -{2}[f]Hh -{2}[g]Hh -f_equivI -sig_equivI.
 Qed.
 
-Lemma pure_internal_eq {A : ofe SI} (x y : A) : ⌜x ≡ y⌝ ⊢ x ≡ y.
+Lemma pure_internal_eq {A : ofe} (x y : A) : ⌜x ≡ y⌝ ⊢ x ≡ y.
 Proof. apply pure_elim'=> ->. apply internal_eq_refl. Qed.
-Lemma discrete_eq {A : ofe SI} (a b : A) : Discrete a → a ≡ b ⊣⊢ ⌜a ≡ b⌝.
+Lemma discrete_eq {A : ofe} (a b : A) : Discrete a → a ≡ b ⊣⊢ ⌜a ≡ b⌝.
 Proof.
   intros. apply (anti_symm _); auto using discrete_eq_1, pure_internal_eq.
 Qed.
 
-Lemma absorbingly_internal_eq {A : ofe SI} (x y : A) : <absorb> (x ≡ y) ⊣⊢ x ≡ y.
+Lemma absorbingly_internal_eq {A : ofe} (x y : A) : <absorb> (x ≡ y) ⊣⊢ x ≡ y.
 Proof.
   apply (anti_symm _), absorbingly_intro.
   apply wand_elim_r', (internal_eq_rewrite' x y (λ y, True -∗ x ≡ y)%I); auto.
   apply wand_intro_l, internal_eq_refl.
 Qed.
-Lemma persistently_internal_eq {A : ofe SI} (a b : A) : <pers> (a ≡ b) ⊣⊢ a ≡ b.
+Lemma persistently_internal_eq {A : ofe} (a b : A) : <pers> (a ≡ b) ⊣⊢ a ≡ b.
 Proof.
   apply (anti_symm (⊢)).
   { by rewrite persistently_into_absorbingly absorbingly_internal_eq. }
@@ -216,33 +216,33 @@ Proof.
   rewrite -(internal_eq_refl emp%I a). apply persistently_emp_intro.
 Qed.
 
-Global Instance internal_eq_absorbing {A : ofe SI} (x y : A) :
+Global Instance internal_eq_absorbing {A : ofe} (x y : A) :
   Absorbing (PROP:=PROP) (x ≡ y).
 Proof. by rewrite /Absorbing absorbingly_internal_eq. Qed.
-Global Instance internal_eq_persistent {A : ofe SI} (a b : A) :
+Global Instance internal_eq_persistent {A : ofe} (a b : A) :
   Persistent (PROP:=PROP) (a ≡ b).
 Proof. by intros; rewrite /Persistent persistently_internal_eq. Qed.
 
 (* Equality under a later. *)
-Lemma internal_eq_rewrite_contractive {A : ofe SI} a b (Ψ : A → PROP)
+Lemma internal_eq_rewrite_contractive {A : ofe} a b (Ψ : A → PROP)
   {HΨ : Contractive Ψ} : ▷ (a ≡ b) ⊢ Ψ a → Ψ b.
 Proof.
   rewrite f_equivI_contractive. apply (internal_eq_rewrite (Ψ a) (Ψ b) id _).
 Qed.
-Lemma internal_eq_rewrite_contractive' {A : ofe SI} a b (Ψ : A → PROP) P
+Lemma internal_eq_rewrite_contractive' {A : ofe} a b (Ψ : A → PROP) P
   {HΨ : Contractive Ψ} : (P ⊢ ▷ (a ≡ b)) → (P ⊢ Ψ a) → P ⊢ Ψ b.
 Proof.
   rewrite later_equivI_2. move: HΨ=>/contractive_alt [g [? HΨ]]. rewrite !HΨ.
   by apply internal_eq_rewrite'.
 Qed.
 
-Lemma later_equivI {A : ofe SI} (x y : A) : Next x ≡ Next y ⊣⊢ ▷ (x ≡ y).
+Lemma later_equivI {A : ofe} (x y : A) : Next x ≡ Next y ⊣⊢ ▷ (x ≡ y).
 Proof. apply (anti_symm _); auto using later_equivI_1, later_equivI_2. Qed.
 Lemma later_equivI_prop_2 `{!Contractive (bi_later (PROP:=PROP))} P Q :
   ▷ (P ≡ Q) ⊢ (▷ P) ≡ (▷ Q).
 Proof. apply (f_equivI_contractive _). Qed.
 
-Global Instance eq_timeless `{!BiTimeless PROP} {A : ofe SI} (a b : A) :
+Global Instance eq_timeless `{!BiTimeless PROP} {A : ofe} (a b : A) :
   Discrete a → Timeless (PROP:=PROP) (a ≡ b).
 Proof. intros. rewrite /Discrete !discrete_eq. apply (timeless _). Qed.
 End internal_eq_derived.
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index 8a47ed61d227445115f884aab4d16cb4b3738810..2b67892e58f8da2102ced571ac55de2aaaabad14 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -13,7 +13,7 @@ Global Instance: Params (@plainly) 2 := {}.
 Notation "â–  P" := (plainly P) : bi_scope.
 
 (* Mixins allow us to create instances easily without having to use Program *)
-Record BiPlainlyMixin {SI: indexT} (PROP : bi SI) `(Plainly PROP) := {
+Record BiPlainlyMixin `{SI: indexT} (PROP : bi) `(Plainly PROP) := {
   bi_plainly_mixin_plainly_ne : NonExpansive (plainly (A:=PROP));
 
   bi_plainly_mixin_plainly_mono (P Q : PROP) : (P ⊢ Q) → ■ P ⊢ ■ Q;
@@ -38,14 +38,14 @@ Record BiPlainlyMixin {SI: indexT} (PROP : bi SI) `(Plainly PROP) := {
   bi_plainly_mixin_later_plainly_2 (P : PROP) : ■ ▷ P ⊢ ▷ ■ P;
 }.
 
-Class BiPlainly {SI: indexT} (PROP : bi SI) := {
+Class BiPlainly `{SI: indexT} (PROP : bi) := {
   bi_plainly_plainly :> Plainly PROP;
   bi_plainly_mixin : BiPlainlyMixin PROP bi_plainly_plainly;
 }.
 Global Hint Mode BiPlainly - ! : typeclass_instances.
 Global Arguments bi_plainly_plainly {_} _ : simpl never.
 
-Class BiPlainlyExist {SI} {PROP: bi SI} `{!BiPlainly PROP} :=
+Class BiPlainlyExist `{SI: indexT} {PROP: bi} `{!BiPlainly PROP} :=
   plainly_exist_1 A (Ψ : A → PROP) :
     ■ (∃ a, Ψ a) ⊢ ∃ a, ■ (Ψ a).
 Global Arguments BiPlainlyExist : clear implicits.
@@ -53,7 +53,7 @@ Global Arguments BiPlainlyExist {_} _ {_}.
 Global Arguments plainly_exist_1 {_} _ {_ _} _.
 Global Hint Mode BiPlainlyExist - ! - : typeclass_instances.
 
-Class BiPropExt {SI} {PROP: bi SI} `{!BiPlainly PROP, !BiInternalEq PROP} :=
+Class BiPropExt `{SI: indexT} {PROP: bi} `{!BiPlainly PROP, !BiInternalEq PROP} :=
   prop_ext_2 (P Q : PROP) : ■ (P ∗-∗ Q) ⊢ P ≡ Q.
 Global Arguments BiPropExt : clear implicits.
 Global Arguments BiPropExt {_} _ {_ _}.
@@ -62,7 +62,7 @@ Global Hint Mode BiPropExt - ! - - : typeclass_instances.
 
 
 Section plainly_laws.
-  Context {SI} {PROP: bi SI} `{!BiPlainly PROP}.
+  Context `{SI: indexT} {PROP: bi} `{!BiPlainly PROP}.
   Implicit Types P Q : PROP.
 
   Global Instance plainly_ne : NonExpansive (@plainly PROP _).
@@ -92,23 +92,23 @@ Section plainly_laws.
 End plainly_laws.
 
 (* Derived properties and connectives *)
-Class Plain {SI} {PROP: bi SI} `{!BiPlainly PROP} (P : PROP) := plain : P ⊢ ■ P.
+Class Plain `{SI: indexT} {PROP: bi} `{!BiPlainly PROP} (P : PROP) := plain : P ⊢ ■ P.
 Global Arguments Plain {_ _ _} _%I : simpl never.
 Global Arguments plain {_ _ _} _%I {_}.
 Global Hint Mode Plain - + - ! : typeclass_instances.
 Global Instance: Params (@Plain) 2 := {}.
 
-Definition plainly_if {SI} {PROP: bi SI} `{!BiPlainly PROP} (p : bool) (P : PROP) : PROP :=
+Definition plainly_if `{SI: indexT} {PROP: bi} `{!BiPlainly PROP} (p : bool) (P : PROP) : PROP :=
   (if p then â–  P else P)%I.
 Global Arguments plainly_if {_ _ _} !_ _%I /.
 Global Instance: Params (@plainly_if) 3 := {}.
-Typeclasses Opaque plainly_if.
+Global Typeclasses Opaque plainly_if.
 
 Notation "â– ? p P" := (plainly_if p P) : bi_scope.
 
 (* Derived laws *)
 Section plainly_derived.
-Context {SI} {PROP: bi SI} `{!BiPlainly PROP}.
+Context `{SI: indexT} {PROP: bi} `{!BiPlainly PROP}.
 Implicit Types P : PROP.
 
 Local Hint Resolve pure_intro forall_intro : core.
@@ -382,7 +382,7 @@ Proof.
   - apply persistently_mono, wand_intro_l. by rewrite sep_and impl_elim_r.
 Qed.
 
-Global Instance limit_preserving_Plain {A:ofe SI} `{!Cofe A} (Φ : A → PROP) :
+Global Instance limit_preserving_Plain {A:ofe} `{!Cofe A} (Φ : A → PROP) :
   NonExpansive Φ → LimitPreserving (λ x, Plain (Φ x)).
 Proof. intros. apply limit_preserving_entails; solve_proper. Qed.
 
@@ -559,7 +559,7 @@ Qed.
 Section internal_eq.
   Context `{!BiInternalEq PROP}.
 
-  Lemma plainly_internal_eq {A:ofe SI} (a b : A) : ■ (a ≡ b) ⊣⊢@{PROP} a ≡ b.
+  Lemma plainly_internal_eq {A: ofe} (a b : A) : ■ (a ≡ b) ⊣⊢@{PROP} a ≡ b.
   Proof.
     apply (anti_symm (⊢)).
     { by rewrite plainly_elim. }
@@ -567,7 +567,7 @@ Section internal_eq.
     rewrite -(internal_eq_refl True%I a) plainly_pure; auto.
   Qed.
 
-  Global Instance internal_eq_plain {A : ofe SI} (a b : A) :
+  Global Instance internal_eq_plain {A : ofe} (a b : A) :
     Plain (PROP:=PROP) (a ≡ b).
   Proof. by intros; rewrite /Plain plainly_internal_eq. Qed.
 End internal_eq.
diff --git a/theories/bi/satisfiable.v b/theories/bi/satisfiable.v
index 44900d8f30f9734c993af74f3c63919ab23143c1..51133da810e9b9ed95bd73b3c47573ae8cb9964f 100644
--- a/theories/bi/satisfiable.v
+++ b/theories/bi/satisfiable.v
@@ -9,7 +9,7 @@ Import derived_laws.bi.
 Import derived_laws_later.bi.
 
 Section satisfiable.
-  Context {SI: indexT} {PROP: bi SI}.
+  Context `{SI: indexT} {PROP: bi}.
 
   Class Satisfiable (sat: PROP → Prop) := {
     sat_mono P Q: (P ⊢ Q) → sat P →  sat Q;
diff --git a/theories/bi/telescopes.v b/theories/bi/telescopes.v
index 9884150153dd71703b2d218e7629a69cd1d9d283..c3998cdd3052e68a4797b611dcad786ea374645d 100644
--- a/theories/bi/telescopes.v
+++ b/theories/bi/telescopes.v
@@ -6,10 +6,10 @@ Import bi.
 (* This cannot import the proofmode because it is imported by the proofmode! *)
 
 (** Telescopic quantifiers *)
-Definition bi_texist {SI} {PROP : bi SI} {TT : tele} (Ψ : TT → PROP) : PROP :=
+Definition bi_texist `{SI: indexT} {PROP : bi} {TT : tele} (Ψ : TT → PROP) : PROP :=
   tele_fold (@bi_exist SI PROP) (λ x, x) (tele_bind Ψ).
 Global Arguments bi_texist {_ _ !_} _ /.
-Definition bi_tforall {SI} {PROP : bi SI} {TT : tele} (Ψ : TT → PROP) : PROP :=
+Definition bi_tforall `{SI: indexT} {PROP : bi} {TT : tele} (Ψ : TT → PROP) : PROP :=
   tele_fold (@bi_forall SI PROP) (λ x, x) (tele_bind Ψ).
 Global Arguments bi_tforall {_ _ !_} _ /.
 
@@ -21,7 +21,7 @@ Notation "'∀..' x .. y , P" := (bi_tforall (λ x, .. (bi_tforall (λ y, P)) ..
   format "∀..  x  ..  y ,  P") : bi_scope.
 
 Section telescopes.
-  Context {SI} {PROP : bi SI} {TT : tele}.
+  Context `{SI: indexT} {PROP : bi} {TT : tele}.
   Implicit Types Ψ : TT → PROP.
 
   Lemma bi_tforall_forall Ψ : bi_tforall Ψ ⊣⊢ bi_forall Ψ.
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 84156150371812112e430e5f9828b913e53db0e1..279f0a1592beaf6b04f44218017187fcf8031f00 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -59,7 +59,7 @@ Notation "P ={ E }▷=∗^ n Q" := (P ={E}[E]▷=∗^n Q) (only parsing) : stdpp
 
 (** Bundled versions  *)
 (* Mixins allow us to create instances easily without having to use Program *)
-Record BiBUpdMixin {SI: indexT} (PROP : bi SI) `(BUpd PROP) := {
+Record BiBUpdMixin `{SI: indexT} (PROP : bi) `(BUpd PROP) := {
   bi_bupd_mixin_bupd_ne : NonExpansive (bupd (PROP:=PROP));
   bi_bupd_mixin_bupd_intro (P : PROP) : P ==∗ P;
   bi_bupd_mixin_bupd_mono (P Q : PROP) : (P ⊢ Q) → (|==> P) ==∗ Q;
@@ -67,7 +67,7 @@ Record BiBUpdMixin {SI: indexT} (PROP : bi SI) `(BUpd PROP) := {
   bi_bupd_mixin_bupd_frame_r (P R : PROP) : (|==> P) ∗ R ==∗ P ∗ R;
 }.
 
-Record BiFUpdMixin {SI: indexT} (PROP : bi SI) `(FUpd PROP) := {
+Record BiFUpdMixin `{SI: indexT} (PROP : bi) `(FUpd PROP) := {
   bi_fupd_mixin_fupd_ne E1 E2 : NonExpansive (fupd (PROP:=PROP) E1 E2);
   bi_fupd_mixin_fupd_intro_mask E1 E2 (P : PROP) : E2 ⊆ E1 → P ⊢ |={E1,E2}=> |={E2,E1}=> P;
   bi_fupd_mixin_except_0_fupd E1 E2 (P : PROP) : ◇ (|={E1,E2}=> P) ={E1,E2}=∗ P;
@@ -78,25 +78,25 @@ Record BiFUpdMixin {SI: indexT} (PROP : bi SI) `(FUpd PROP) := {
   bi_fupd_mixin_fupd_frame_r E1 E2 (P R : PROP) : (|={E1,E2}=> P) ∗ R ={E1,E2}=∗ P ∗ R;
 }.
 
-Class BiBUpd {SI: indexT} (PROP : bi SI) := {
+Class BiBUpd `{SI: indexT} (PROP : bi) := {
   bi_bupd_bupd :> BUpd PROP;
   bi_bupd_mixin : BiBUpdMixin PROP bi_bupd_bupd;
 }.
 Global Hint Mode BiBUpd - ! : typeclass_instances.
 Global Arguments bi_bupd_bupd : simpl never.
 
-Class BiFUpd {SI: indexT} (PROP : bi SI) := {
+Class BiFUpd `{SI: indexT} (PROP : bi) := {
   bi_fupd_fupd :> FUpd PROP;
   bi_fupd_mixin : BiFUpdMixin PROP bi_fupd_fupd;
 }.
 Global Hint Mode BiFUpd - ! : typeclass_instances.
 Global Arguments bi_fupd_fupd : simpl never.
 
-Class BiBUpdFUpd {SI: indexT} (PROP : bi SI) `{BiBUpd SI PROP, BiFUpd SI PROP} :=
+Class BiBUpdFUpd `{SI: indexT} (PROP : bi) `{!BiBUpd PROP, !BiFUpd PROP} :=
   bupd_fupd E (P : PROP) : (|==> P) ={E}=∗ P.
 Global Hint Mode BiBUpdFUpd - ! - - : typeclass_instances.
 
-Class BiBUpdPlainly {SI: indexT} (PROP : bi SI) `{!BiBUpd PROP, !BiPlainly PROP} :=
+Class BiBUpdPlainly `{SI: indexT} (PROP : bi) `{!BiBUpd PROP, !BiPlainly PROP} :=
   bupd_plainly (P : PROP) : (|==> ■ P) -∗ P.
 Global Hint Mode BiBUpdPlainly - ! - - : typeclass_instances.
 
@@ -104,7 +104,7 @@ Global Hint Mode BiBUpdPlainly - ! - - : typeclass_instances.
 only make sense for affine logics. From the axioms below, one could derive
 [■ P ={E}=∗ P] (see the lemma [fupd_plainly_elim]), which in turn gives
 [True ={E}=∗ emp]. *)
-Class BiFUpdPlainly {SI: indexT} (PROP : bi SI) `{!BiFUpd PROP, !BiPlainly PROP} := {
+Class BiFUpdPlainly {SI: indexT} (PROP : bi) `{!BiFUpd PROP, !BiPlainly PROP} := {
   (** When proving a fancy update of a plain proposition, you can also prove it
   while being allowed to open all invariants. *)
   fupd_plainly_mask_empty E (P : PROP) :
@@ -126,7 +126,7 @@ Class BiFUpdPlainly {SI: indexT} (PROP : bi SI) `{!BiFUpd PROP, !BiPlainly PROP}
 Global Hint Mode BiBUpdFUpd - ! - - : typeclass_instances.
 
 Section bupd_laws.
-  Context {SI} {PROP: bi SI} `{!BiBUpd PROP}.
+  Context `{SI: indexT} {PROP: bi} `{!BiBUpd PROP}.
   Implicit Types P : PROP.
 
   Global Instance bupd_ne : NonExpansive (@bupd PROP _).
@@ -142,7 +142,7 @@ Section bupd_laws.
 End bupd_laws.
 
 Section fupd_laws.
-  Context {SI} {PROP: bi SI} `{!BiFUpd PROP}.
+  Context `{SI: indexT} {PROP: bi} `{!BiFUpd PROP}.
   Implicit Types P : PROP.
 
   Global Instance fupd_ne E1 E2 : NonExpansive (@fupd PROP _ E1 E2).
@@ -163,7 +163,7 @@ Section fupd_laws.
 End fupd_laws.
 
 Section bupd_derived.
-  Context {SI} {PROP: bi SI} `{!BiBUpd PROP}.
+  Context `{SI: indexT} {PROP: bi} `{!BiBUpd PROP}.
   Implicit Types P Q R : PROP.
 
   (* FIXME: Removing the `PROP:=` diverges. *)
@@ -232,7 +232,7 @@ Section bupd_derived.
 End bupd_derived.
 
 Section fupd_derived.
-  Context {SI} {PROP: bi SI} `{!BiFUpd PROP}.
+  Context `{SI: indexT} {PROP: bi} `{!BiFUpd PROP}.
   Implicit Types P Q R : PROP.
 
   Global Instance fupd_proper E1 E2 :