diff --git a/theories/base_logic/algebra.v b/theories/base_logic/algebra.v
index 4e7be3a2b1c511784f4f75f2a22203f18138ed66..2a0d85a93d74505cc327d11a4a1108822475071d 100644
--- a/theories/base_logic/algebra.v
+++ b/theories/base_logic/algebra.v
@@ -7,18 +7,18 @@ From iris.prelude Require Import options.
 Local Coercion uPred_holds : uPred >-> Funclass.
 
 Section upred.
-Context {SI} {M : ucmra SI}.
+Context `{SI: indexT} {M : ucmra}.
 
 (* Force implicit argument M *)
 Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
 Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
 
-Lemma prod_validI {A B : cmra SI} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
+Lemma prod_validI {A B : cmra} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
 Proof. by uPred.unseal. Qed.
-Lemma option_validI {A : cmra SI} (mx : option A) :
+Lemma option_validI {A : cmra} (mx : option A) :
   ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True : uPred M end.
 Proof. uPred.unseal. by destruct mx. Qed.
-Lemma discrete_fun_validI {A} {B : A → ucmra SI} (g : discrete_fun B) :
+Lemma discrete_fun_validI {A} {B : A → ucmra} (g : discrete_fun B) :
   ✓ g ⊣⊢ ∀ i, ✓ g i.
 Proof. by uPred.unseal. Qed.
 
@@ -26,7 +26,7 @@ Lemma frac_validI (q : Qp) : ✓ q ⊣⊢ ⌜q ≤ 1⌝%Qp.
 Proof. rewrite uPred.discrete_valid frac_valid' //. Qed.
 
 Section gmap_ofe.
-  Context `{Countable K} {A : ofe SI}.
+  Context `{Countable K} {A : ofe}.
   Implicit Types m : gmap K A.
   Implicit Types i : K.
 
@@ -35,7 +35,7 @@ Section gmap_ofe.
 End gmap_ofe.
 
 Section gmap_cmra.
-  Context `{Countable K} {A : cmra SI}.
+  Context `{Countable K} {A : cmra}.
   Implicit Types m : gmap K A.
 
   Lemma gmap_validI m : ✓ m ⊣⊢ ∀ i, ✓ (m !! i).
@@ -52,7 +52,7 @@ Section gmap_cmra.
 End gmap_cmra.
 
 Section list_ofe.
-  Context {A : ofe SI}.
+  Context {A : ofe}.
   Implicit Types l : list A.
 
   Lemma list_equivI l1 l2 : l1 ≡ l2 ⊣⊢ ∀ i, l1 !! i ≡ l2 !! i.
@@ -60,7 +60,7 @@ Section list_ofe.
 End list_ofe.
 
 Section list_cmra.
-  Context {A : ucmra SI}.
+  Context {A : ucmra}.
   Implicit Types l : list A.
 
   Lemma list_validI l : ✓ l ⊣⊢ ∀ i, ✓ (l !! i).
@@ -68,7 +68,7 @@ Section list_cmra.
 End list_cmra.
 
 Section excl.
-  Context {A : ofe SI}.
+  Context {A : ofe}.
   Implicit Types a b : A.
   Implicit Types x y : excl A.
 
@@ -89,7 +89,7 @@ Section excl.
 End excl.
 
 Section agree.
-  Context {A : ofe SI}.
+  Context {A : ofe}.
   Implicit Types a b : A.
   Implicit Types x y : agree A.
 
@@ -107,7 +107,7 @@ Section agree.
 End agree.
 
 Section csum_ofe.
-  Context {A B : ofe SI}.
+  Context {A B : ofe}.
   Implicit Types a : A.
   Implicit Types b : B.
 
@@ -125,7 +125,7 @@ Section csum_ofe.
 End csum_ofe.
 
 Section csum_cmra.
-  Context {A B : cmra SI}.
+  Context {A B : cmra}.
   Implicit Types a : A.
   Implicit Types b : B.
 
@@ -139,7 +139,7 @@ Section csum_cmra.
 End csum_cmra.
 
 Section view.
-  Context {A: ofe SI} {B: ucmra SI} (rel : view_rel A B).
+  Context {A: ofe} {B: ucmra} (rel : view_rel A B).
   Implicit Types a : A.
   Implicit Types ag : option (frac * agree A).
   Implicit Types b : B.
@@ -204,7 +204,7 @@ Section view.
 End view.
 
 Section auth.
-  Context {A : ucmra SI}.
+  Context {A : ucmra}.
   Implicit Types a b : A.
   Implicit Types x y : auth A.
 
@@ -236,7 +236,7 @@ Section auth.
 End auth.
 
 Section excl_auth.
-  Context {A : ofe SI}.
+  Context {A : ofe}.
   Implicit Types a b : A.
 
   Lemma excl_auth_agreeI a b : ✓ (●E a ⋅ ◯E b) ⊢ (a ≡ b).
@@ -248,7 +248,7 @@ Section excl_auth.
 End excl_auth.
 
 Section gmap_view.
-  Context {K : Type} `{Countable K} {V : ofe SI}.
+  Context {K : Type} `{Countable K} {V : ofe}.
   Implicit Types (m : gmap K V) (k : K) (dq : dfrac) (v : V).
 
   Lemma gmap_view_both_validI m k dq v :
@@ -261,7 +261,7 @@ Section gmap_view.
 
   Lemma gmap_view_frag_op_validI k dq1 dq2 v1 v2 :
     ✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ⊣⊢
-    ✓ ((dq1: dfracR SI) ⋅ dq2) ∧ v1 ≡ v2.
+    ✓ (dq1 ⋅ dq2) ∧ v1 ≡ v2.
   Proof.
     rewrite /gmap_view_frag -view_frag_op. apply view_frag_validI=> n x.
     rewrite gmap_view.gmap_view_rel_exists singleton_op singleton_validN.
diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index a7c9be29ea284f10aaaae0405fb56d5809a0415c..65234c9d5f0777058953aeac47aaf9d1189f457e 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -6,11 +6,11 @@ Import uPred_primitive.
 (** BI instances for [uPred], and re-stating the remaining primitive laws in
 terms of the BI interface. This file does *not* unseal. *)
 
-Definition uPred_emp {SI: indexT} {M: ucmra SI} : uPred M := uPred_pure True.
+Definition uPred_emp `{SI: indexT} {M: ucmra} : uPred M := uPred_pure True.
 
 Local Existing Instance entails_po.
 
-Lemma uPred_bi_mixin {SI: indexT} (M : ucmra SI) :
+Lemma uPred_bi_mixin `{SI: indexT} (M : ucmra) :
   BiMixin
     uPred_entails uPred_emp uPred_pure uPred_and uPred_or uPred_impl
     (@uPred_forall SI M) (@uPred_exist SI M) uPred_sep uPred_wand
@@ -66,7 +66,7 @@ Proof.
   - exact: persistently_and_sep_l_1.
 Qed.
 
-Lemma uPred_bi_later_mixin {SI} (M : ucmra SI) :
+Lemma uPred_bi_later_mixin `{SI: indexT} (M : ucmra) :
   BiLaterMixin
     uPred_entails uPred_pure uPred_or uPred_impl
     (@uPred_forall SI M) uPred_sep uPred_persistently uPred_later.
@@ -82,18 +82,18 @@ Proof.
   - exact: later_false_em.
 Qed.
 
-Canonical Structure uPredI {SI} (M : ucmra SI) : bi SI :=
-  {| bi_ofe_mixin := ofe_mixin_of SI (uPred M);
+Canonical Structure uPredI `{SI: indexT} (M : ucmra) : bi :=
+  {| bi_ofe_mixin := ofe_mixin_of (uPred M);
      bi_bi_mixin := uPred_bi_mixin M;
      bi_bi_later_mixin := uPred_bi_later_mixin M |}.
 
-Global Instance uPred_pure_forall {SI} (M : ucmra SI) : BiPureForall (uPredI M).
+Global Instance uPred_pure_forall `{SI: indexT} (M : ucmra) : BiPureForall (uPredI M).
 Proof. exact: @pure_forall_2. Qed.
 
-Global Instance uPred_later_contractive {SI} (M : ucmra SI) : BiLaterContractive (uPredI M).
+Global Instance uPred_later_contractive `{SI: indexT} (M : ucmra) : BiLaterContractive (uPredI M).
 Proof. apply later_contractive. Qed.
 
-Lemma uPred_internal_eq_mixin {SI} (M : ucmra SI) : BiInternalEqMixin (uPredI M) (@uPred_internal_eq SI M).
+Lemma uPred_internal_eq_mixin `{SI: indexT} (M : ucmra) : BiInternalEqMixin (uPredI M) (@uPred_internal_eq SI M).
 Proof.
   split.
   - exact: internal_eq_ne.
@@ -105,10 +105,10 @@ Proof.
   - exact: @later_eq_1.
   - exact: @later_eq_2.
 Qed.
-Global Instance uPred_internal_eq {SI} (M : ucmra SI) : BiInternalEq (uPredI M) :=
+Global Instance uPred_internal_eq `{SI: indexT} (M : ucmra) : BiInternalEq (uPredI M) :=
   {| bi_internal_eq_mixin := uPred_internal_eq_mixin M |}.
 
-Lemma uPred_plainly_mixin {SI} (M : ucmra SI) : BiPlainlyMixin (uPredI M) uPred_plainly.
+Lemma uPred_plainly_mixin `{SI: indexT} (M : ucmra) : BiPlainlyMixin (uPredI M) uPred_plainly.
 Proof.
   split.
   - exact: plainly_ne.
@@ -132,13 +132,13 @@ Proof.
   - exact: later_plainly_1.
   - exact: later_plainly_2.
 Qed.
-Global Instance uPred_plainly {SI} (M : ucmra SI) : BiPlainly (uPredI M) :=
+Global Instance uPred_plainly `{SI: indexT} (M : ucmra) : BiPlainly (uPredI M) :=
   {| bi_plainly_mixin := uPred_plainly_mixin M |}.
 
-Global Instance uPred_prop_ext {SI} (M : ucmra SI) : BiPropExt (uPredI M).
+Global Instance uPred_prop_ext `{SI: indexT} (M : ucmra) : BiPropExt (uPredI M).
 Proof. exact: prop_ext_2. Qed.
 
-Lemma uPred_bupd_mixin {SI} (M : ucmra SI) : BiBUpdMixin (uPredI M) uPred_bupd.
+Lemma uPred_bupd_mixin `{SI: indexT} (M : ucmra) : BiBUpdMixin (uPredI M) uPred_bupd.
 Proof.
   split.
   - exact: bupd_ne.
@@ -147,24 +147,24 @@ Proof.
   - exact: bupd_trans.
   - exact: bupd_frame_r.
 Qed.
-Global Instance uPred_bi_bupd {SI} (M : ucmra SI) : BiBUpd (uPredI M) := {| bi_bupd_mixin := uPred_bupd_mixin M |}.
+Global Instance uPred_bi_bupd `{SI: indexT} (M : ucmra) : BiBUpd (uPredI M) := {| bi_bupd_mixin := uPred_bupd_mixin M |}.
 
-Global Instance uPred_bi_bupd_plainly {SI} (M : ucmra SI) : BiBUpdPlainly (uPredI M).
+Global Instance uPred_bi_bupd_plainly `{SI: indexT} (M : ucmra) : BiBUpdPlainly (uPredI M).
 Proof. exact: bupd_plainly. Qed.
 
-Global Instance uPred_bi_finite {SI} `{!FiniteIndex SI} (M : ucmra SI): BiFinite (uPredI M).
+Global Instance uPred_bi_finite `{SI: indexT} `{!FiniteIndex SI} (M : ucmra): BiFinite (uPredI M).
 Proof.
   split.
   - intros; apply later_exist_false.
   - exact: later_sep_1.
 Qed.
 
-Global Instance uPred_bi_later_or {SI} `{!FiniteBoundedExistential SI} (M : ucmra SI): BiLaterOr (uPredI M).
+Global Instance uPred_bi_later_or `{SI: indexT} `{!FiniteBoundedExistential SI} (M : ucmra): BiLaterOr (uPredI M).
 Proof.
   split. exact: later_or_2.
 Qed.
 
-Global Instance uPred_bi_timeless {SI} (M : ucmra SI): BiTimeless (uPredI M).
+Global Instance uPred_bi_timeless `{SI: indexT} (M : ucmra): BiTimeless (uPredI M).
 Proof.
   split.
   - exact: pure_timeless.
@@ -172,31 +172,31 @@ Proof.
   - intros X; apply: later_exist_timeless.
 Qed.
 
-Global Instance uPred_sat_instance {SI} (M : ucmra SI): Satisfiable (@uPred_sat SI M).
+Global Instance uPred_sat_instance `{SI: indexT} (M : ucmra): Satisfiable (@uPred_sat SI M).
 Proof.
   split.
   - apply uPred_sat_mono.
   - apply uPred_sat_elim.
 Qed.
 
-Global Instance uPred_sat_bupd_instance {SI} (M : ucmra SI): SatisfiableBUpd (@uPred_sat SI M).
+Global Instance uPred_sat_bupd_instance `{SI: indexT} (M : ucmra): SatisfiableBUpd (@uPred_sat SI M).
 Proof. split. apply uPred_sat_bupd. Qed.
 
-Global Instance uPred_sat_later_instance {SI} (M : ucmra SI): SatisfiableLater (@uPred_sat SI M).
+Global Instance uPred_sat_later_instance `{SI: indexT} (M : ucmra): SatisfiableLater (@uPred_sat SI M).
 Proof. split. apply uPred_sat_later. Qed.
 
-Global Instance uPred_sat_exists_instance {SI} (M : ucmra SI) {X} `{!TypeExistentialProperty X SI}: SatisfiableExists X (@uPred_sat SI M).
+Global Instance uPred_sat_exists_instance `{SI: indexT} (M : ucmra) {X} `{!TypeExistentialProperty X SI}: SatisfiableExists X (@uPred_sat SI M).
 Proof. split. apply uPred_sat_exists, _. Qed.
 
 (** extra BI instances *)
 
-Global Instance uPred_affine {SI} (M : ucmra SI) : BiAffine (uPredI M) | 0.
+Global Instance uPred_affine `{SI: indexT} (M : ucmra) : BiAffine (uPredI M) | 0.
 Proof. intros P. exact: pure_intro. Qed.
 (* Also add this to the global hint database, otherwise [eauto] won't work for
 many lemmas that have [BiAffine] as a premise. *)
 Global Hint Immediate uPred_affine : core.
 
-Global Instance uPred_plainly_exist_1 {SI} (M : ucmra SI) : BiPlainlyExist (uPredI M).
+Global Instance uPred_plainly_exist_1 `{SI: indexT} (M : ucmra) : BiPlainlyExist (uPredI M).
 Proof. exact: @plainly_exist_1. Qed.
 
 (** Re-state/export lemmas about Iris-specific primitive connectives (own, valid) *)
@@ -204,7 +204,7 @@ Proof. exact: @plainly_exist_1. Qed.
 Module uPred.
 
 Section restate.
-Context {SI} {M : ucmra SI}.
+Context `{SI: indexT} {M : ucmra}.
 Implicit Types φ : Prop.
 Implicit Types P Q : uPred M.
 Implicit Types A : Type.
@@ -214,7 +214,7 @@ Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
 Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
 
 Global Instance ownM_ne : NonExpansive (@uPred_ownM SI M) := uPred_primitive.ownM_ne.
-Global Instance cmra_valid_ne {A : cmra SI} : NonExpansive (@uPred_cmra_valid SI M A)
+Global Instance cmra_valid_ne {A : cmra} : NonExpansive (@uPred_cmra_valid SI M A)
   := uPred_primitive.cmra_valid_ne.
 
 (** Re-exporting primitive lemmas that are not in any interface *)
@@ -235,28 +235,28 @@ Proof. exact: uPred_primitive.bupd_ownM_updateP. Qed.
 between two [siProp], but we do not have the infrastructure
 to express the more general case. This temporary proof rule will
 be replaced by the proper one eventually. *)
-Lemma internal_eq_entails {A B : ofe SI} (a1 a2 : A) (b1 b2 : B) :
+Lemma internal_eq_entails {A B : ofe} (a1 a2 : A) (b1 b2 : B) :
   (∀ n, a1 ≡{n}≡ a2 → b1 ≡{n}≡ b2) → a1 ≡ a2 ⊢ b1 ≡ b2.
 Proof. exact: uPred_primitive.internal_eq_entails. Qed.
 
 Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a.
 Proof. exact: uPred_primitive.ownM_valid. Qed.
-Lemma cmra_valid_intro {A : cmra SI} P (a : A) : ✓ a → P ⊢ (✓ a).
+Lemma cmra_valid_intro {A : cmra} P (a : A) : ✓ a → P ⊢ (✓ a).
 Proof. exact: uPred_primitive.cmra_valid_intro. Qed.
-Lemma cmra_valid_elim {A : cmra SI} (a : A) : ¬ ✓{zero} a → ✓ a ⊢ False.
+Lemma cmra_valid_elim {A : cmra} (a : A) : ¬ ✓{zero} a → ✓ a ⊢ False.
 Proof. exact: uPred_primitive.cmra_valid_elim. Qed.
-Lemma plainly_cmra_valid_1 {A : cmra SI} (a : A) : ✓ a ⊢ ■ ✓ a.
+Lemma plainly_cmra_valid_1 {A : cmra} (a : A) : ✓ a ⊢ ■ ✓ a.
 Proof. exact: uPred_primitive.plainly_cmra_valid_1. Qed.
-Lemma cmra_valid_weaken {A : cmra SI} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
+Lemma cmra_valid_weaken {A : cmra} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
 Proof. exact: uPred_primitive.cmra_valid_weaken. Qed.
-Lemma discrete_valid {A : cmra SI} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ a⌝.
+Lemma discrete_valid {A : cmra} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ a⌝.
 Proof. exact: uPred_primitive.discrete_valid. Qed.
 
 (** This is really just a special case of an entailment
 between two [siProp], but we do not have the infrastructure
 to express the more general case. This temporary proof rule will
 be replaced by the proper one eventually. *)
-Lemma valid_entails {A B : cmra SI} (a : A) (b : B) :
+Lemma valid_entails {A B : cmra} (a : A) (b : B) :
   (∀ n, ✓{n} a → ✓{n} b) → ✓ a ⊢ ✓ b.
 Proof. exact: uPred_primitive.valid_entails. Qed.
 
@@ -268,7 +268,7 @@ Proof. apply: uPred_primitive.uPred_ownM_timeless. Qed.
 Lemma pure_soundness φ : (⊢@{uPredI M} ⌜ φ ⌝) → φ.
 Proof. apply pure_soundness. Qed.
 
-Lemma internal_eq_soundness {A : ofe SI} (x y : A) : (⊢@{uPredI M} x ≡ y) → x ≡ y.
+Lemma internal_eq_soundness {A : ofe} (x y : A) : (⊢@{uPredI M} x ≡ y) → x ≡ y.
 Proof. apply internal_eq_soundness. Qed.
 
 Lemma later_soundness P : (⊢ ▷ P) → ⊢ P.
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index fc979d4a1c681f7ca5f37f3afbfa814995276cfe..205e9fcb0a92b0ae5875f19a78336c7c1eb721f5 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -9,7 +9,7 @@ Import bi.bi base_logic.bi.uPred.
 
 Module uPred.
 Section derived.
-Context {SI} {M : ucmra SI}.
+Context `{SI: indexT} {M : ucmra}.
 Implicit Types φ : Prop.
 Implicit Types P Q : uPred M.
 Implicit Types A : Type.
@@ -20,11 +20,11 @@ Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
 
 (** Propers *)
 Global Instance ownM_proper: Proper ((≡) ==> (⊣⊢)) (@uPred_ownM SI M) := ne_proper _.
-Global Instance cmra_valid_proper {A : cmra SI} :
+Global Instance cmra_valid_proper {A : cmra} :
   Proper ((≡) ==> (⊣⊢)) (@uPred_cmra_valid SI M A) := ne_proper _.
 
 (** Own and valid derived *)
-Lemma persistently_cmra_valid_1 {A : cmra SI} (a : A) : ✓ a ⊢ <pers> (✓ a : uPred M).
+Lemma persistently_cmra_valid_1 {A : cmra} (a : A) : ✓ a ⊢ <pers> (✓ a : uPred M).
 Proof. by rewrite {1}plainly_cmra_valid_1 plainly_elim_persistently. Qed.
 Lemma intuitionistically_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
 Proof.
@@ -38,9 +38,9 @@ Global Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM SI M).
 Proof. intros a b [b' ->]. by rewrite ownM_op sep_elim_l. Qed.
 Lemma ownM_unit' : uPred_ownM ε ⊣⊢ True.
 Proof. apply (anti_symm _); first by apply pure_intro. apply ownM_unit. Qed.
-Lemma plainly_cmra_valid {A : cmra SI} (a : A) : ■ ✓ a ⊣⊢ ✓ a.
+Lemma plainly_cmra_valid {A : cmra} (a : A) : ■ ✓ a ⊣⊢ ✓ a.
 Proof. apply (anti_symm _), plainly_cmra_valid_1. apply plainly_elim, _. Qed.
-Lemma intuitionistically_cmra_valid {A : cmra SI} (a : A) : □ ✓ a ⊣⊢ ✓ a.
+Lemma intuitionistically_cmra_valid {A : cmra} (a : A) : □ ✓ a ⊣⊢ ✓ a.
 Proof.
   rewrite /bi_intuitionistically affine_affinely. intros; apply (anti_symm _);
     first by rewrite persistently_elim.
@@ -53,17 +53,17 @@ Proof.
 Qed.
 
 (** Timeless instances *)
-Global Instance valid_timeless {A : cmra SI} `{!CmraDiscrete A} (a : A) :
+Global Instance valid_timeless {A : cmra} `{!CmraDiscrete A} (a : A) :
   Timeless (✓ a : uPred M)%I.
 Proof. rewrite /Timeless !discrete_valid. apply (timeless _). Qed.
 
 (** Plainness *)
-Global Instance cmra_valid_plain {A : cmra SI} (a : A) :
+Global Instance cmra_valid_plain {A : cmra} (a : A) :
   Plain (✓ a : uPred M)%I.
 Proof. rewrite /Persistent. apply plainly_cmra_valid_1. Qed.
 
 (** Persistence *)
-Global Instance cmra_valid_persistent {A : cmra SI} (a : A) :
+Global Instance cmra_valid_persistent {A : cmra} (a : A) :
   Persistent (✓ a : uPred M)%I.
 Proof. rewrite /Persistent. apply persistently_cmra_valid_1. Qed.
 Global Instance ownM_persistent a : CoreId a → Persistent (@uPred_ownM SI M a).
diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index a7d47d411f60a7319ba673f417555685ab550ac0..74a59511160cb84fc266f1cba4ac311ed4c2e332 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -5,14 +5,14 @@ From iris.base_logic.lib Require Export invariants.
 From iris.prelude Require Import options.
 Import uPred.
 
-Class cinvG {SI} Σ := cinv_inG :> inG Σ (fracR SI).
-Definition cinvΣ SI : gFunctors SI := #[GFunctor (fracR SI)].
+Class cinvG `{SI: indexT} Σ := cinv_inG :> inG Σ fracR.
+Definition cinvΣ `{SI: indexT} : gFunctors := #[GFunctor fracR].
 
-Global Instance subG_cinvΣ {SI} {Σ} : subG (cinvΣ SI) Σ → cinvG Σ.
+Global Instance subG_cinvΣ `{SI: indexT} {Σ} : subG (cinvΣ) Σ → cinvG Σ.
 Proof. solve_inG. Qed.
 
 Section defs.
-  Context {SI} {Σ : gFunctors SI} `{!invG Σ, !cinvG Σ}.
+  Context `{SI: indexT} {Σ : gFunctors} `{!invG Σ, !cinvG Σ}.
 
   Definition cinv_own (γ : gname) (p : frac) : iProp Σ := own γ p.
 
@@ -23,7 +23,7 @@ End defs.
 Global Instance: Params (@cinv) 6 := {}.
 
 Section proofs.
-  Context {SI} {Σ : gFunctors SI} `{!invG Σ, !cinvG Σ}.
+  Context `{SI: indexT} {Σ : gFunctors} `{!invG Σ, !cinvG Σ}.
 
   Global Instance cinv_own_timeless γ p : Timeless (cinv_own γ p).
   Proof. rewrite /cinv_own; apply _. Qed.
@@ -108,7 +108,7 @@ Section proofs.
   Qed.
 
   (*** Accessors *)
-  Lemma cinv_acc_strong `{FiniteBoundedExistential SI}  E N γ p P :
+  Lemma cinv_acc_strong `{!FiniteBoundedExistential SI}  E N γ p P :
     ↑N ⊆ E →
     cinv N γ P -∗ (cinv_own γ p ={E,E∖↑N}=∗
     ▷ P ∗ cinv_own γ p ∗ (∀ E' : coPset, ▷ P ∨ cinv_own γ 1 ={E',↑N ∪ E'}=∗ True)).
@@ -125,7 +125,7 @@ Section proofs.
     - iDestruct (cinv_own_1_l with "Hown' Hown") as %[].
   Qed.
 
-  Lemma cinv_acc `{FiniteBoundedExistential SI} E N γ p P :
+  Lemma cinv_acc `{!FiniteBoundedExistential SI} E N γ p P :
     ↑N ⊆ E →
     cinv N γ P -∗ cinv_own γ p ={E,E∖↑N}=∗ ▷ P ∗ cinv_own γ p ∗ (▷ P ={E∖↑N,E}=∗ True).
   Proof.
@@ -137,7 +137,7 @@ Section proofs.
   Qed.
 
   (*** Other *)
-  Lemma cinv_cancel `{FiniteBoundedExistential SI} E N γ P : ↑N ⊆ E → cinv N γ P -∗ cinv_own γ 1 ={E}=∗ ▷ P.
+  Lemma cinv_cancel `{!FiniteBoundedExistential SI} E N γ P : ↑N ⊆ E → cinv N γ P -∗ cinv_own γ 1 ={E}=∗ ▷ P.
   Proof.
     iIntros (?) "#Hinv Hγ".
     iMod (cinv_acc_strong with "Hinv Hγ") as "($ & Hγ & H)"; first done.
@@ -147,7 +147,7 @@ Section proofs.
 
   Global Instance into_inv_cinv N γ P : IntoInv (cinv N γ P) N := {}.
 
-  Global Instance into_acc_cinv `{FiniteBoundedExistential SI} E N γ P p :
+  Global Instance into_acc_cinv `{!FiniteBoundedExistential SI} E N γ P p :
     IntoAcc (X:=unit) (cinv N γ P)
             (↑N ⊆ E) (cinv_own γ p) (fupd E (E∖↑N)) (fupd (E∖↑N) E)
             (λ _, ▷ P ∗ cinv_own γ p)%I (λ _, ▷ P)%I (λ _, None)%I.
@@ -158,4 +158,4 @@ Section proofs.
   Qed.
 End proofs.
 
-Typeclasses Opaque cinv_own cinv.
+Global Typeclasses Opaque cinv_own cinv.
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index 21b44164fc40177ff594d57d87e78e2e6b0da616..f8d6af92d6375a075aa677eccf074057b97eacfd 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -7,15 +7,15 @@ From iris.prelude Require Import options.
 Export invG.
 Import uPred.
 
-Definition uPred_fupd_def {SI} {Σ: gFunctors SI} `{!invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
+Definition uPred_fupd_def `{SI : indexT} {Σ: gFunctors} `{!invG Σ} (E1 E2 : coPset) (P : iProp Σ) : iProp Σ :=
   (wsat ∗ ownE E1 ==∗ ◇ (wsat ∗ ownE E2 ∗ P))%I.
 Definition uPred_fupd_aux : seal (@uPred_fupd_def). Proof. by eexists. Qed.
 Definition uPred_fupd := uPred_fupd_aux.(unseal).
 Global Arguments uPred_fupd {SI Σ _}.
-Lemma uPred_fupd_eq {SI} {Σ: gFunctors SI} `{!invG Σ} : @fupd _ uPred_fupd = uPred_fupd_def.
+Lemma uPred_fupd_eq `{SI : indexT} {Σ: gFunctors} `{!invG Σ} : @fupd _ uPred_fupd = uPred_fupd_def.
 Proof. rewrite -uPred_fupd_aux.(seal_eq) //. Qed.
 
-Lemma uPred_fupd_mixin {SI} {Σ: gFunctors SI} `{!invG Σ} : BiFUpdMixin (uPredI (iResUR Σ)) uPred_fupd.
+Lemma uPred_fupd_mixin `{SI : indexT} {Σ: gFunctors} `{!invG Σ} : BiFUpdMixin (uPredI (iResUR Σ)) uPred_fupd.
 Proof.
   split.
   - rewrite uPred_fupd_eq. solve_proper.
@@ -33,13 +33,13 @@ Proof.
     iIntros "!> !>". by iApply "HP".
   - rewrite uPred_fupd_eq /uPred_fupd_def. by iIntros (????) "[HwP $]".
 Qed.
-Global Instance uPred_bi_fupd {SI} {Σ: gFunctors SI} `{!invG Σ} : BiFUpd (uPredI (iResUR Σ)) :=
+Global Instance uPred_bi_fupd `{SI : indexT} {Σ: gFunctors} `{!invG Σ} : BiFUpd (uPredI (iResUR Σ)) :=
   {| bi_fupd_mixin := uPred_fupd_mixin |}.
 
-Global Instance uPred_bi_bupd_fupd {SI} {Σ: gFunctors SI} `{!invG Σ} : BiBUpdFUpd (uPredI (iResUR Σ)).
+Global Instance uPred_bi_bupd_fupd `{SI : indexT} {Σ: gFunctors} `{!invG Σ} : BiBUpdFUpd (uPredI (iResUR Σ)).
 Proof. rewrite /BiBUpdFUpd uPred_fupd_eq. by iIntros (E P) ">? [$ $] !> !>". Qed.
 
-Global Instance uPred_bi_fupd_plainly {SI} {Σ: gFunctors SI} `{!invG Σ} : BiFUpdPlainly (uPredI (iResUR Σ)).
+Global Instance uPred_bi_fupd_plainly `{SI : indexT} {Σ: gFunctors} `{!invG Σ} : BiFUpdPlainly (uPredI (iResUR Σ)).
 Proof.
   split.
   - rewrite uPred_fupd_eq /uPred_fupd_def. iIntros (E P) "H [Hw HE]".
@@ -60,7 +60,7 @@ Proof.
     by iFrame.
 Qed.
 
-Lemma fupd_plain_soundness {SI} {Σ: gFunctors SI}  `{!invPreG Σ} E1 E2 (P: iProp Σ) `{!Plain P}:
+Lemma fupd_plain_soundness `{SI : indexT} {Σ: gFunctors}  `{!invPreG Σ} E1 E2 (P: iProp Σ) `{!Plain P}:
   (∀ `{Hinv: !invG Σ}, ⊢ |={E1,E2}=> P) → ⊢ P.
 Proof.
   iIntros (Hfupd). apply later_soundness. iMod wsat_alloc as (Hinv) "[Hw HE]".
@@ -70,7 +70,7 @@ Proof.
   iMod ("H" with "[$]") as "[Hw [HE >H']]"; iFrame.
 Qed.
 
-Lemma step_fupdN_soundness {SI} {Σ: gFunctors SI} `{!invPreG Σ} φ n :
+Lemma step_fupdN_soundness `{SI : indexT} {Σ: gFunctors} `{!invPreG Σ} φ n :
   (∀ `{Hinv: !invG Σ}, ⊢@{iPropI Σ} |={⊤}[∅]▷=>^n |={⊤,∅}=> ⌜ φ ⌝) →
   φ.
 Proof.
@@ -88,7 +88,7 @@ Proof.
     iNext. by iMod "Hφ".
 Qed.
 
-Lemma step_fupdN_soundness' {SI} {Σ: gFunctors SI}  `{!invPreG Σ} φ n :
+Lemma step_fupdN_soundness' `{SI : indexT} {Σ: gFunctors}  `{!invPreG Σ} φ n :
   (∀ `{Hinv: !invG Σ}, ⊢@{iPropI Σ} |={⊤}[∅]▷=>^n ⌜ φ ⌝) →
   φ.
 Proof.
diff --git a/theories/base_logic/lib/gen_heap.v b/theories/base_logic/lib/gen_heap.v
index 8e70872267270034f7c6b499fe7188db9855ffec..a2732f2ee7a55e24d1ea083418dcb8660a01cd6d 100644
--- a/theories/base_logic/lib/gen_heap.v
+++ b/theories/base_logic/lib/gen_heap.v
@@ -63,13 +63,13 @@ these can be matched up with the invariant namespaces. *)
 
 (** The CMRAs we need, and the global ghost names we are using. *)
 
-Class gen_heapPreG {SI} (L V : Type) (Σ : gFunctors SI) `{Countable L} := {
-  gen_heap_preG_inG :> inG Σ (gmap_viewR L (leibnizO SI V));
-  gen_meta_preG_inG :> inG Σ (gmap_viewR L (gnameO SI));
-  gen_meta_data_preG_inG :> inG Σ (reservation_mapR (agreeR (positiveO SI)));
+Class gen_heapPreG `{SI: indexT} (L V : Type) (Σ : gFunctors) `{Countable L} := {
+  gen_heap_preG_inG :> inG Σ (gmap_viewR L (leibnizO V));
+  gen_meta_preG_inG :> inG Σ (gmap_viewR L gnameO);
+  gen_meta_data_preG_inG :> inG Σ (reservation_mapR (agreeR positiveO));
 }.
 
-Class gen_heapG {SI} (L V : Type) (Σ : gFunctors SI) `{Countable L} := GenHeapG {
+Class gen_heapG `{SI: indexT} (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapG {
   gen_heap_inG :> gen_heapPreG L V Σ;
   gen_heap_name : gname;
   gen_meta_name : gname
@@ -78,29 +78,29 @@ Global Arguments GenHeapG {SI} L V Σ {_ _ _} _ _.
 Global Arguments gen_heap_name {SI L V Σ _ _} _ : assert.
 Global Arguments gen_meta_name {SI L V Σ _ _} _ : assert.
 
-Definition gen_heapΣ {SI} (L V : Type) `{Countable L} : gFunctors SI := #[
-  GFunctor (gmap_viewR L (leibnizO SI V));
-  GFunctor (gmap_viewR L (gnameO SI));
-  GFunctor (reservation_mapR (agreeR (positiveO SI)))
+Definition gen_heapΣ `{SI: indexT} (L V : Type) `{Countable L} : gFunctors := #[
+  GFunctor (gmap_viewR L (leibnizO V));
+  GFunctor (gmap_viewR L (gnameO));
+  GFunctor (reservation_mapR (agreeR (positiveO)))
 ].
 
-Global Instance subG_gen_heapPreG {SI} {Σ: gFunctors SI} {L V} `{Countable L} :
+Global Instance subG_gen_heapPreG `{SI: indexT} {Σ: gFunctors} {L V} `{Countable L} :
   subG (gen_heapΣ L V) Σ → gen_heapPreG L V Σ.
 Proof. solve_inG. Qed.
 
 
 Section definitions.
-  Context {SI} {Σ: gFunctors SI} `{Countable L, hG : !gen_heapG L V Σ}.
+  Context `{SI: indexT} {Σ: gFunctors} `{Countable L, hG : !gen_heapG L V Σ}.
 
   Definition gen_heap_interp (σ : gmap L V) : iProp Σ := ∃ m: gmap L gname,
     (* The [⊆] is used to avoid assigning ghost information to the locations in
     the initial heap (see [gen_heap_init]). *)
     ⌜ dom m ⊆ dom σ ⌝ ∧
-    own (gen_heap_name hG) (gmap_view_auth 1 (σ : gmap L (leibnizO SI V))) ∗
-    own (gen_meta_name hG) (gmap_view_auth 1 (m : gmap L (gnameO SI))).
+    own (gen_heap_name hG) (gmap_view_auth 1 (σ : gmap L (leibnizO V))) ∗
+    own (gen_meta_name hG) (gmap_view_auth 1 (m : gmap L (gnameO))).
 
   Definition mapsto_def (l : L) (dq : dfrac) (v: V) : iProp Σ :=
-    own (gen_heap_name hG) (gmap_view_frag l dq (v : leibnizO SI V)).
+    own (gen_heap_name hG) (gmap_view_frag l dq (v : leibnizO V)).
   Definition mapsto_aux : seal (@mapsto_def). Proof. by eexists. Qed.
   Definition mapsto := mapsto_aux.(unseal).
   Definition mapsto_eq : @mapsto = @mapsto_def := mapsto_aux.(seal_eq).
@@ -133,7 +133,7 @@ Local Notation "l ↦ v" := (mapsto l (DfracOwn 1) v)
   (at level 20, format "l  ↦  v") : bi_scope.
 
 Section gen_heap.
-  Context {SI} {Σ: gFunctors SI} {L V} `{Countable L, !gen_heapG L V Σ}.
+  Context `{SI: indexT} {Σ: gFunctors} {L V} `{Countable L, !gen_heapG L V Σ}.
   Implicit Types P Q : iProp Σ.
   Implicit Types Φ : V → iProp Σ.
   Implicit Types σ : gmap L V.
@@ -154,12 +154,12 @@ Section gen_heap.
   Global Instance mapsto_persistent l v : Persistent (l ↦□ v).
   Proof. rewrite mapsto_eq. apply _. Qed.
 
-  Lemma mapsto_valid l dq v : l ↦{dq} v -∗ ⌜✓ (dq: dfracR SI)⌝%Qp.
+  Lemma mapsto_valid l dq v : l ↦{dq} v -∗ ⌜✓ dq⌝%Qp.
   Proof.
     rewrite mapsto_eq. iIntros "Hl".
     iDestruct (own_valid with "Hl") as %?%gmap_view_frag_valid. done.
   Qed.
-  Lemma mapsto_valid_2 l dq1 dq2 v1 v2 : l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜✓ ((dq1: dfracR SI) ⋅ dq2) ∧ v1 = v2⌝.
+  Lemma mapsto_valid_2 l dq1 dq2 v1 v2 : l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ ⌜✓ (dq1 ⋅ dq2) ∧ v1 = v2⌝.
   Proof.
     rewrite mapsto_eq. iIntros "H1 H2".
     iDestruct (own_valid_2 with "H1 H2") as %[??]%gmap_view_frag_op_valid_L.
@@ -174,7 +174,7 @@ Section gen_heap.
   Qed.
 
   Lemma mapsto_combine l dq1 dq2 v1 v2 :
-    l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ l ↦{(dq1: dfracR SI) ⋅ dq2} v1 ∗ ⌜v1 = v2⌝.
+    l ↦{dq1} v1 -∗ l ↦{dq2} v2 -∗ l ↦{dq1 ⋅ dq2} v1 ∗ ⌜v1 = v2⌝.
   Proof.
     iIntros "Hl1 Hl2". iDestruct (mapsto_agree with "Hl1 Hl2") as %->.
     iCombine "Hl1 Hl2" as "Hl".
@@ -183,7 +183,7 @@ Section gen_heap.
   Qed.
 
   Lemma mapsto_frac_ne l1 l2 dq1 dq2 v1 v2 :
-    ¬ ✓((dq1: dfracR SI) ⋅ dq2) → l1 ↦{dq1} v1 -∗ l2 ↦{dq2} v2 -∗ ⌜l1 ≠ l2⌝.
+    ¬ ✓(dq1 ⋅ dq2) → l1 ↦{dq1} v1 -∗ l2 ↦{dq2} v2 -∗ ⌜l1 ≠ l2⌝.
   Proof.
     iIntros (?) "Hl1 Hl2"; iIntros (->).
     by iDestruct (mapsto_valid_2 with "Hl1 Hl2") as %[??].
@@ -315,14 +315,14 @@ End gen_heap.
 The key difference to [gen_heap_init] is that the [inG] instances in the new
 [gen_heapG] instance are related to the original [gen_heapPreG] instance,
 whereas [gen_heap_init] forgets about that relation. *)
-Lemma gen_heap_init_names {SI} {Σ: gFunctors SI} `{Countable L, !gen_heapPreG L V Σ} σ :
+Lemma gen_heap_init_names `{SI: indexT} {Σ: gFunctors} `{Countable L, !gen_heapPreG L V Σ} σ :
   ⊢ |==> ∃ γh γm : gname,
     let hG := GenHeapG L V Σ γh γm in
     gen_heap_interp σ ∗ ([∗ map] l ↦ v ∈ σ, l ↦ v) ∗ ([∗ map] l ↦ _ ∈ σ, meta_token l ⊤).
 Proof.
-  iMod (own_alloc (gmap_view_auth 1 (∅ : gmap L (leibnizO SI V)))) as (γh) "Hh".
+  iMod (own_alloc (gmap_view_auth 1 (∅ : gmap L (leibnizO V)))) as (γh) "Hh".
   { exact: gmap_view_auth_valid. }
-  iMod (own_alloc (gmap_view_auth 1 (∅ : gmap L (gnameO SI)))) as (γm) "Hm".
+  iMod (own_alloc (gmap_view_auth 1 (∅ : gmap L (gnameO)))) as (γm) "Hm".
   { exact: gmap_view_auth_valid. }
   iExists γh, γm.
   iAssert (gen_heap_interp (hG:=GenHeapG _ _ _ γh γm) ∅) with "[Hh Hm]" as "Hinterp".
@@ -332,7 +332,7 @@ Proof.
   rewrite right_id_L. done.
 Qed.
 
-Lemma gen_heap_init {SI} {Σ: gFunctors SI} `{Countable L, !gen_heapPreG L V Σ} σ :
+Lemma gen_heap_init `{SI: indexT} {Σ: gFunctors} `{Countable L, !gen_heapPreG L V Σ} σ :
   ⊢ |==> ∃ _ : gen_heapG L V Σ,
     gen_heap_interp σ ∗ ([∗ map] l ↦ v ∈ σ, l ↦ v) ∗ ([∗ map] l ↦ _ ∈ σ, meta_token l ⊤).
 Proof.
@@ -348,17 +348,17 @@ Definition γ_gen_heap_meta : gname := encode "gen_heap.meta".
 Definition gen_heap_gnames : coPset := {[ γ_gen_heap; γ_gen_heap_meta ]}.
 
 (* mirrors gen_heapPreG but for type class inference reasons we do not reuse gen_heapPreG *)
-Class gen_heapS {SI} (L V : Type) (Σ : gFunctors SI) `{Countable L} := {
+Class gen_heapS {SI} (L V : Type) (Σ : gFunctors) `{Countable L} := {
   gen_heapS_inG :> inG Σ (authR (gen_heapUR SI L V));
   gen_heapS_meta_inG :> inG Σ (authR (gen_metaUR SI L));
   gen_heapS_data_inG :> inG Σ (reservation_mapR (agreeR (positiveO SI)))
 }.
 
-Instance gen_heapS_gen_heapG {SI} {Σ : gFunctors SI} `{Countable L} `{gen_heapS SI L V Σ} : gen_heapG L V Σ :=
+Instance gen_heapS_gen_heapG {SI} {Σ : gFunctors} `{Countable L} `{gen_heapS SI L V Σ} : gen_heapG L V Σ :=
   GenHeapG _ _ _ _ _ _ _ _ _ γ_gen_heap γ_gen_heap_meta.
 
 
-Lemma alloc_gen_heap {SI} {Σ : gFunctors SI} L V `{Countable L} `{gen_heapPreG SI L V Σ} (σ: gmap L V):
+Lemma alloc_gen_heap {SI} {Σ : gFunctors} L V `{Countable L} `{gen_heapPreG SI L V Σ} (σ: gmap L V):
   sbi_emp_valid (|==> ∃ γ_gen_heap γ_gen_heap_meta, let H := GenHeapG SI L V _ _ _ _ _ _ γ_gen_heap γ_gen_heap_meta in gen_heap_interp σ)%I.
 Proof.
   iMod (own_alloc (● to_gen_heap SI σ)) as (γ_gen_heap) "H1".
@@ -370,7 +370,7 @@ Proof.
   iFrame "H1 H2". by rewrite dom_empty_L.
 Qed.
 
-Lemma heap_init_to_bigOp {SI} {Σ : gFunctors SI} `{hG: gen_heapG SI L V Σ} σ:
+Lemma heap_init_to_bigOp {SI} {Σ : gFunctors} `{hG: gen_heapG SI L V Σ} σ:
   own (gen_heap_name hG) (◯ (to_gen_heap SI σ)) -∗
       [∗ map] i ↦ v ∈ σ, i ↦ v .
 Proof.
@@ -390,7 +390,7 @@ Proof.
     by iApply IHσ.
 Qed.
 
-Lemma alloc_gen_heap_strong {SI} {Σ : gFunctors SI} L V `{Countable L} `{gen_heapPreG SI L V Σ} (σ: gmap L V):
+Lemma alloc_gen_heap_strong {SI} {Σ : gFunctors} L V `{Countable L} `{gen_heapPreG SI L V Σ} (σ: gmap L V):
   sbi_emp_valid (|==> ∃ γ_gen_heap γ_gen_heap_meta, let H := GenHeapG SI L V _ _ _ _ _ _ γ_gen_heap γ_gen_heap_meta in gen_heap_interp σ ∗ [∗ map] i↦v ∈ σ, i ↦ v)%I.
 Proof.
   iMod (own_alloc (● to_gen_heap SI σ ⋅ ◯ to_gen_heap SI σ)) as (γ_gen_heap) "(H1&Hfrag)".
@@ -403,7 +403,7 @@ Proof.
   - by iApply heap_init_to_bigOp.
 Qed.
 
-Lemma initial_gen_heap {SI} {Σ : gFunctors SI} L V `{Countable L} `{gen_heapS SI L V Σ} (σ: gmap L V):
+Lemma initial_gen_heap {SI} {Σ : gFunctors} L V `{Countable L} `{gen_heapS SI L V Σ} (σ: gmap L V):
   initial gen_heap_gnames (gen_heap_interp σ)%I.
 Proof.
   feed pose proof (initial_alloc γ_gen_heap (● to_gen_heap SI σ)) as HH.
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index f606021224d10472b27818c20cf9a38a67ddd65d..466ed7f5f5331929b6516820559c6c8d0ed5f3d9 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -7,7 +7,7 @@ From iris.prelude Require Import options.
 Import uPred.
 
 (** Semantic Invariants *)
-Definition inv_def {SI} {Σ: gFunctors SI}  `{!invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
+Definition inv_def `{SI : indexT} {Σ: gFunctors}  `{!invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
   (□ ∀ E, ⌜↑N ⊆ E⌝ → |={E,E ∖ ↑N}=> ▷ P ∗ (▷ P ={E ∖ ↑N,E}=∗ True))%I.
 Definition inv_aux : seal (@inv_def). Proof. by eexists. Qed.
 Definition inv := inv_aux.(unseal).
@@ -17,7 +17,7 @@ Global Instance: Params (@inv) 4 := {}.
 
 (** * Invariants *)
 Section inv.
-  Context {SI} {Σ: gFunctors SI}  `{!invG Σ}.
+  Context `{SI : indexT} {Σ: gFunctors}  `{!invG Σ}.
   Implicit Types i : positive.
   Implicit Types N : namespace.
   Implicit Types E : coPset.
@@ -97,7 +97,7 @@ Section inv.
   Global Instance inv_persistent N P : Persistent (inv N P).
   Proof. rewrite inv_eq. apply _. Qed.
 
-  Lemma inv_alter `{FiniteIndex SI} N P Q : inv N P -∗ ▷ □ (P -∗ Q ∗ (Q -∗ P)) -∗ inv N Q.
+  Lemma inv_alter `{!FiniteIndex SI} N P Q : inv N P -∗ ▷ □ (P -∗ Q ∗ (Q -∗ P)) -∗ inv N Q.
   Proof.
     rewrite inv_eq. iIntros "#HI #HPQ !>" (E Hsub).
     iMod ("HI" $! E Hsub) as "[HP Hclose]".
@@ -132,7 +132,7 @@ Section inv.
     rewrite inv_eq /inv_def; iIntros (?) "#HI". by iApply "HI".
   Qed.
 
-  Lemma inv_combine `{FiniteIndex SI} N1 N2 N P Q :
+  Lemma inv_combine `{!FiniteIndex SI} N1 N2 N P Q :
     N1 ## N2 →
     ↑N1 ∪ ↑N2 ⊆@{coPset} ↑N →
     inv N1 P -∗ inv N2 Q -∗ inv N (P ∗ Q).
@@ -145,7 +145,7 @@ Section inv.
     iMod "Hclose" as %_. iMod ("HcloseQ" with "HQ") as %_. by iApply "HcloseP".
   Qed.
 
-  Lemma inv_combine_dup_l `{FiniteIndex SI} N P Q :
+  Lemma inv_combine_dup_l `{!FiniteIndex SI} N P Q :
     □ (P -∗ P ∗ P) -∗
     inv N P -∗ inv N Q -∗ inv N (P ∗ Q).
   Proof.
@@ -190,16 +190,16 @@ Section inv.
     iIntros "!> {$HP} HP". iApply "Hclose"; auto.
   Qed.
 
-  Lemma inv_split_l `{FiniteIndex SI} N P Q : inv N (P ∗ Q) -∗ inv N P.
+  Lemma inv_split_l `{!FiniteIndex SI} N P Q : inv N (P ∗ Q) -∗ inv N P.
   Proof.
     iIntros "#HI". iApply (inv_alter with "HI").
     iIntros "!> !> [$ $] $".
   Qed.
-  Lemma inv_split_r `{FiniteIndex SI} N P Q : inv N (P ∗ Q) -∗ inv N Q.
+  Lemma inv_split_r `{!FiniteIndex SI} N P Q : inv N (P ∗ Q) -∗ inv N Q.
   Proof.
     rewrite (comm _ P Q). eapply inv_split_l.
   Qed.
-  Lemma inv_split `{FiniteIndex SI} N P Q : inv N (P ∗ Q) -∗ inv N P ∗ inv N Q.
+  Lemma inv_split `{!FiniteIndex SI} N P Q : inv N (P ∗ Q) -∗ inv N P ∗ inv N Q.
   Proof.
     iIntros "#H".
     iPoseProof (inv_split_l with "H") as "$".
diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v
index 26e39d122fe8d12a31d4a5abaee1f6facb91661b..1606f9a35f8a6e468aee0e19d54077ce27822f4d 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -24,12 +24,12 @@ the agreement CMRA. *)
 (** * Locally contractive functors *)
 (** The type [gFunctor] bundles a functor from the category of COFEs to the
 category of CMRAs with a proof that it is locally contractive. *)
-Structure gFunctor (SI: indexT) := GFunctor {
-  gFunctor_F :> rFunctor SI;
+Structure gFunctor `{SI: indexT} := GFunctor {
+  gFunctor_F :> rFunctor;
   gFunctor_map_contractive : rFunctorContractive gFunctor_F;
 }.
 Global Arguments GFunctor {_} _ {_}.
-Existing Instance gFunctor_map_contractive.
+Global Existing Instance gFunctor_map_contractive.
 Add Printing Constructor gFunctor.
 
 (** The type [gFunctors] describes the parameters [Σ] of the Iris logic: lists
@@ -38,16 +38,16 @@ of [gFunctor]s.
 Note that [gFunctors] is isomorphic to [list gFunctor], but defined in an
 alternative way to avoid universe inconsistencies with respect to the universe
 monomorphic [list] type. *)
-Definition gFunctors SI := { n : nat & fin n → gFunctor SI }.
+Definition gFunctors `{SI: indexT} := { n : nat & fin n → gFunctor }.
 
-Definition gid {SI} (Σ : gFunctors SI) := fin (projT1 Σ).
-Definition gFunctors_lookup {SI} (Σ : gFunctors SI) : gid Σ → gFunctor SI := projT2 Σ.
+Definition gid `{SI: indexT} (Σ : gFunctors) := fin (projT1 Σ).
+Definition gFunctors_lookup `{SI: indexT} (Σ : gFunctors) : gid Σ → gFunctor := projT2 Σ.
 
 Definition gname := positive.
-Canonical Structure gnameO SI := leibnizO SI gname.
+Canonical Structure gnameO `{SI: indexT} := leibnizO gname.
 
 (** The resources functor [iResF Σ A := ∀ i : gid, gname -fin-> (Σ i) A]. *)
-Definition iResF {SI} (Σ : gFunctors SI) : urFunctor SI :=
+Definition iResF `{SI: indexT} (Σ : gFunctors) : urFunctor :=
   discrete_funURF (λ i, gmapURF gname (gFunctors_lookup Σ i)).
 
 
@@ -55,12 +55,12 @@ Definition iResF {SI} (Σ : gFunctors SI) : urFunctor SI :=
 functors, and the append operator on lists of functors. These are used to
 compose [gFunctors] out of smaller pieces. *)
 Module gFunctors.
-  Definition nil {SI} : gFunctors SI := existT 0 (fin_0_inv _).
+  Definition nil `{SI: indexT} : gFunctors := existT 0 (fin_0_inv _).
 
-  Definition singleton {SI} (F : gFunctor SI) : gFunctors SI :=
-    existT 1 (fin_S_inv (λ _, gFunctor SI) F (fin_0_inv _)).
+  Definition singleton `{SI: indexT} (F : gFunctor) : gFunctors :=
+    existT 1 (fin_S_inv (λ _, gFunctor) F (fin_0_inv _)).
 
-  Definition app {SI} (Σ1 Σ2 : gFunctors SI) : gFunctors SI :=
+  Definition app `{SI: indexT} (Σ1 Σ2 : gFunctors) : gFunctors :=
     existT (projT1 Σ1 + projT1 Σ2) (fin_add_inv _ (projT2 Σ1) (projT2 Σ2)).
 End gFunctors.
 
@@ -80,7 +80,7 @@ lock invariant.
 
 The contraints to can be expressed using the type class [subG Σ1 Σ2], which
 expresses that the functors [Σ1] are contained in [Σ2]. *)
-Class subG {SI} (Σ1 Σ2 : gFunctors SI) := in_subG i :
+Class subG `{SI: indexT} (Σ1 Σ2 : gFunctors) := in_subG i :
   { j | gFunctors_lookup Σ1 i = gFunctors_lookup Σ2 j }.
 
 (** Avoid trigger happy type class search: this line ensures that type class
@@ -90,21 +90,21 @@ their first parameter to avoid loops. For example, the instances [subG_authΣ]
 and [auth_discrete] otherwise create a cycle that pops up arbitrarily. *)
 Global Hint Mode subG - ! + : typeclass_instances.
 
-Lemma subG_inv {SI} (Σ1 Σ2 Σ: gFunctors SI) : subG (gFunctors.app Σ1 Σ2) Σ → subG Σ1 Σ * subG Σ2 Σ.
+Lemma subG_inv `{SI: indexT} (Σ1 Σ2 Σ: gFunctors) : subG (gFunctors.app Σ1 Σ2) Σ → subG Σ1 Σ * subG Σ2 Σ.
 Proof.
   move=> H; split.
   - move=> i; move: H=> /(_ (Fin.L _ i)) [j] /=. rewrite fin_add_inv_l; eauto.
   - move=> i; move: H=> /(_ (Fin.R _ i)) [j] /=. rewrite fin_add_inv_r; eauto.
 Qed.
 
-Global Instance subG_refl {SI} (Σ: gFunctors SI) : subG Σ Σ.
+Global Instance subG_refl `{SI: indexT} (Σ: gFunctors) : subG Σ Σ.
 Proof. move=> i; by exists i. Qed.
-Global Instance subG_app_l {SI} (Σ Σ1 Σ2: gFunctors SI) : subG Σ Σ1 → subG Σ (gFunctors.app Σ1 Σ2).
+Global Instance subG_app_l `{SI: indexT} (Σ Σ1 Σ2: gFunctors) : subG Σ Σ1 → subG Σ (gFunctors.app Σ1 Σ2).
 Proof.
   move=> H i; move: H=> /(_ i) [j ?].
   exists (Fin.L _ j). by rewrite /= fin_add_inv_l.
 Qed.
-Global Instance subG_app_r {SI} (Σ Σ1 Σ2 : gFunctors SI): subG Σ Σ2 → subG Σ (gFunctors.app Σ1 Σ2).
+Global Instance subG_app_r `{SI: indexT} (Σ Σ1 Σ2 : gFunctors): subG Σ Σ2 → subG Σ (gFunctors.app Σ1 Σ2).
 Proof.
   move=> H i; move: H=> /(_ i) [j ?].
   exists (Fin.R _ j). by rewrite /= fin_add_inv_r.
@@ -116,50 +116,50 @@ Qed.
 the construction, this way we are sure we do not use any properties of the
 construction, and also avoid Coq from blindly unfolding it. *)
 Module Type iProp_solution_sig.
-  Parameter iPrePropO : ∀ {SI: indexT}, gFunctors SI → ofe SI.
-  Global Declare Instance iPreProp_cofe {SI}{Σ: gFunctors SI} : Cofe (iPrePropO Σ).
+  Parameter iPrePropO : ∀ {SI: indexT}, gFunctors → ofe.
+  Global Declare Instance iPreProp_cofe `{SI: indexT} {Σ: gFunctors} : Cofe (iPrePropO Σ).
 
-  Definition iResUR {SI} (Σ : gFunctors SI) : ucmra SI :=
+  Definition iResUR `{SI: indexT} (Σ : gFunctors) : ucmra :=
     discrete_funUR (λ i,
       gmapUR gname (rFunctor_apply (gFunctors_lookup Σ i) (iPrePropO Σ))).
   Notation iProp Σ := (uPred (iResUR Σ)).
   Notation iPropO Σ := (uPredO (iResUR Σ)).
   Notation iPropI Σ := (uPredI (iResUR Σ)).
 
-  Parameter iProp_unfold: ∀ {SI} {Σ: gFunctors SI}, iPropO Σ -n> iPrePropO Σ.
-  Parameter iProp_fold: ∀ {SI} {Σ: gFunctors SI}, iPrePropO Σ -n> iPropO Σ.
-  Parameter iProp_fold_unfold: ∀ {SI} {Σ: gFunctors SI} (P : iProp Σ),
+  Parameter iProp_unfold: ∀ `{SI: indexT} {Σ: gFunctors}, iPropO Σ -n> iPrePropO Σ.
+  Parameter iProp_fold: ∀ `{SI: indexT} {Σ: gFunctors}, iPrePropO Σ -n> iPropO Σ.
+  Parameter iProp_fold_unfold: ∀ `{SI: indexT} {Σ: gFunctors} (P : iProp Σ),
     iProp_fold (iProp_unfold P) ≡ P.
-  Parameter iProp_unfold_fold: ∀ {SI} {Σ: gFunctors SI} (P : iPrePropO Σ),
+  Parameter iProp_unfold_fold: ∀ `{SI: indexT} {Σ: gFunctors} (P : iPrePropO Σ),
     iProp_unfold (iProp_fold P) ≡ P.
 End iProp_solution_sig.
 
 Module Export iProp_solution : iProp_solution_sig.
   Import cofe_solver.
   (* TODO: checkc this *)
-  Definition iProp_result {SI} (Σ : gFunctors SI) :
-    solution (uPredOF (iResF Σ)) := solver.solution_F _ (uPredOF (iResF Σ)) (uPred_pure True).
-  Definition iPrePropO {SI} (Σ : gFunctors SI) : ofe SI := iProp_result Σ.
-  Global Instance iPreProp_cofe {SI} {Σ: gFunctors SI} : Cofe (iPrePropO Σ) := _.
+  Definition iProp_result `{SI: indexT} (Σ : gFunctors) :
+    solution (uPredOF (iResF Σ)) := solver.solution_F (uPredOF (iResF Σ)) (uPred_pure True).
+  Definition iPrePropO `{SI: indexT} (Σ : gFunctors) : ofe := iProp_result Σ.
+  Global Instance iPreProp_cofe `{SI: indexT} {Σ: gFunctors} : Cofe (iPrePropO Σ) := _.
 
-  Definition iResUR {SI} (Σ : gFunctors SI) : ucmra SI :=
+  Definition iResUR `{SI: indexT} (Σ : gFunctors) : ucmra :=
     discrete_funUR (λ i,
       gmapUR gname (rFunctor_apply (gFunctors_lookup Σ i) (iPrePropO Σ))).
   Notation iProp Σ := (uPred (iResUR Σ)).
   Notation iPropO Σ := (uPredO (iResUR Σ)).
 
-  Definition iProp_unfold {SI} {Σ: gFunctors SI} : iPropO Σ -n> iPrePropO Σ :=
+  Definition iProp_unfold `{SI: indexT} {Σ: gFunctors} : iPropO Σ -n> iPrePropO Σ :=
     solution_fold _ (iProp_result Σ).
-  Definition iProp_fold {SI} {Σ: gFunctors SI} : iPrePropO Σ -n> iPropO Σ := solution_unfold _ _.
-  Lemma iProp_fold_unfold {SI} {Σ: gFunctors SI} (P : iProp Σ) : iProp_fold (iProp_unfold P) ≡ P.
+  Definition iProp_fold `{SI: indexT} {Σ: gFunctors} : iPrePropO Σ -n> iPropO Σ := solution_unfold _ _.
+  Lemma iProp_fold_unfold `{SI: indexT} {Σ: gFunctors} (P : iProp Σ) : iProp_fold (iProp_unfold P) ≡ P.
   Proof. apply @solution_unfold_fold. Qed.
-  Lemma iProp_unfold_fold {SI} {Σ: gFunctors SI} (P : iPrePropO Σ) : iProp_unfold (iProp_fold P) ≡ P.
+  Lemma iProp_unfold_fold `{SI: indexT} {Σ: gFunctors} (P : iPrePropO Σ) : iProp_unfold (iProp_fold P) ≡ P.
   Proof. apply @solution_fold_unfold. Qed.
 End iProp_solution.
 
 
 (** * Properties of the solution to the recursive domain equation *)
-Lemma iProp_unfold_equivI {SI} {Σ: gFunctors SI} (P Q : iProp Σ) :
+Lemma iProp_unfold_equivI `{SI: indexT} {Σ: gFunctors} (P Q : iProp Σ) :
   iProp_unfold P ≡ iProp_unfold Q ⊢@{iPropI Σ} P ≡ Q.
 Proof.
   rewrite -{2}(iProp_fold_unfold P) -{2}(iProp_fold_unfold Q).
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index b77660e2e0f2d60a63dc231130d1919a49149df8..adf6352ee39d3ee188482e375414b00043b96b74 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -8,15 +8,15 @@ Import uPred.
 
 Definition na_inv_pool_name := gname.
 
-Class na_invG {SI} Σ :=
-  na_inv_inG :> inG Σ (prodR (coPset_disjR SI) (gset_disjR positive)).
-Definition na_invΣ {SI} : gFunctors SI :=
-  #[ GFunctor (constRF (prodR (coPset_disjR SI) (gset_disjR positive))) ].
-Global Instance subG_na_invG {SI} {Σ: gFunctors SI} : subG na_invΣ Σ → na_invG Σ.
+Class na_invG `{SI: indexT} Σ :=
+  na_inv_inG :> inG Σ (prodR coPset_disjR (gset_disjR positive)).
+Definition na_invΣ `{SI: indexT} : gFunctors :=
+  #[ GFunctor (constRF (prodR coPset_disjR (gset_disjR positive))) ].
+Global Instance subG_na_invG `{SI: indexT} {Σ: gFunctors} : subG na_invΣ Σ → na_invG Σ.
 Proof. solve_inG. Qed.
 
 Section defs.
-  Context {SI} {Σ: gFunctors SI} `{!invG Σ, !na_invG Σ}.
+  Context `{SI: indexT} {Σ: gFunctors} `{!invG Σ, !na_invG Σ}.
 
   Definition na_own (p : na_inv_pool_name) (E : coPset) : iProp Σ :=
     own p (CoPset E, GSet ∅).
@@ -27,10 +27,10 @@ Section defs.
 End defs.
 
 Global Instance: Params (@na_inv) 3 := {}.
-Typeclasses Opaque na_own na_inv.
+Global Typeclasses Opaque na_own na_inv.
 
 Section proofs.
-  Context {SI} {Σ: gFunctors SI} `{!invG Σ, !na_invG Σ}.
+  Context `{SI: indexT} {Σ: gFunctors} `{!invG Σ, !na_invG Σ}.
 
   Global Instance na_own_timeless p E : Timeless (na_own p E).
   Proof. rewrite /na_own; apply _. Qed.
@@ -76,7 +76,7 @@ Section proofs.
   Lemma na_inv_alloc p E N P : ▷ P ={E}=∗ na_inv p N P.
   Proof.
     iIntros "HP".
-    iMod (own_unit (prodUR (coPset_disjUR SI) (gset_disjUR positive)) p) as "Hempty".
+    iMod (own_unit (prodUR coPset_disjUR (gset_disjUR positive)) p) as "Hempty".
     iMod (own_updateP with "Hempty") as ([m1 m2]) "[Hm Hown]".
     { apply prod_updateP'.
       - apply cmra_updateP_id, (reflexivity (R:=eq)).
@@ -92,7 +92,7 @@ Section proofs.
     iNext. iLeft. by iFrame.
   Qed.
 
-  Lemma na_inv_acc `{FiniteIndex SI} p E F N P :
+  Lemma na_inv_acc `{!FiniteIndex SI} p E F N P :
     ↑N ⊆ E → ↑N ⊆ F →
     na_inv p N P -∗ na_own p F ={E}=∗ ▷ P ∗ na_own p (F∖↑N) ∗
                        (▷ P ∗ na_own p (F∖↑N) ={E}=∗ na_own p F).
@@ -114,7 +114,7 @@ Section proofs.
 
   Global Instance into_inv_na p N P : IntoInv (na_inv p N P) N := {}.
 
-  Global Instance into_acc_na `{FiniteIndex SI} p F E N P :
+  Global Instance into_acc_na `{!FiniteIndex SI} p F E N P :
     IntoAcc (X:=unit) (na_inv p N P)
             (↑N ⊆ E ∧ ↑N ⊆ F) (na_own p F) (fupd E E) (fupd E E)
             (λ _, ▷ P ∗ na_own p (F∖↑N))%I (λ _, ▷ P ∗ na_own p (F∖↑N))%I
@@ -162,7 +162,7 @@ Section proofs.
     intros ???. iIntros "HI Hna". iApply (na_inv_acc_open_timeless_weakening with "HI Hna"); auto.
   Qed.
 
-  Lemma na_inv_acc_open `{FiniteBoundedExistential SI} p E F N P :
+  Lemma na_inv_acc_open `{!FiniteBoundedExistential SI} p E F N P :
     ↑N ⊆ E → ↑N ⊆ F →
     na_inv p N P -∗ na_own p F ={E}=∗ ▷ (P ∗ na_own p (F∖↑N)
                     ∗ (▷ P ∗ na_own p (F∖↑N) -∗ |={E}=> na_own p F)).
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index bb3ba2e5ff34b6230d0dc5ccc14a6b9da0a2dccd..655cd3250f4b85461ed99076b1ed472c8666e252 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -10,7 +10,7 @@ Import uPred.
 individual CMRAs instead of (lists of) CMRA *functors*. This additional class is
 needed because Coq is otherwise unable to solve type class constraints due to
 higher-order unification problems. *)
-Class inG {SI} (Σ : gFunctors SI) (A : cmra SI) := InG {
+Class inG `{SI: indexT} (Σ : gFunctors) (A : cmra) := InG {
   inG_id : gid Σ;
   inG_apply := rFunctor_apply (gFunctors_lookup Σ inG_id);
   inG_prf : A = inG_apply (iPropO Σ) _;
@@ -23,7 +23,7 @@ mode [!] for [A] since we can have multiple [inG]s for different [A]s, so we do
 not want Coq to pick one arbitrarily. *)
 Global Hint Mode inG - - ! : typeclass_instances.
 
-Lemma subG_inG {SI} Σ (F : gFunctor SI) : subG F Σ → inG Σ (rFunctor_apply F (iPropO Σ)).
+Lemma subG_inG `{SI: indexT} Σ (F : gFunctor) : subG F Σ → inG Σ (rFunctor_apply F (iPropO Σ)).
 Proof. move=> /(_ 0%fin) /= [j ->]. by exists j. Qed.
 
 (** This tactic solves the usual obligations "subG ? Σ → {in,?}G ? Σ" *)
@@ -58,19 +58,19 @@ Ltac solve_inG :=
   split; (assumption || by apply _).
 
 (** * Definition of the connective [own] *)
-Local Definition inG_unfold {SI} {Σ: gFunctors SI} {A} {i : inG Σ A} :
+Local Definition inG_unfold `{SI: indexT} {Σ: gFunctors} {A} {i : inG Σ A} :
     inG_apply i (iPropO Σ) -n> inG_apply i (iPrePropO Σ) :=
   rFunctor_map _ (iProp_fold, iProp_unfold).
-Local Definition inG_fold {SI} {Σ: gFunctors SI} {A} {i : inG Σ A} :
+Local Definition inG_fold `{SI: indexT} {Σ: gFunctors} {A} {i : inG Σ A} :
     inG_apply i (iPrePropO Σ) -n> inG_apply i (iPropO Σ) :=
   rFunctor_map _ (iProp_unfold, iProp_fold).
 
-Local Definition iRes_singleton {SI} {Σ: gFunctors SI} {A} {i : inG Σ A} (γ : gname) (a : A) : iResUR Σ :=
+Local Definition iRes_singleton `{SI: indexT} {Σ: gFunctors} {A} {i : inG Σ A} (γ : gname) (a : A) : iResUR Σ :=
   discrete_fun_singleton (inG_id i)
     {[ γ := inG_unfold (cmra_transport inG_prf a) ]}.
 Global Instance: Params (@iRes_singleton) 4 := {}.
 
-Local Definition own_def {SI} {Σ: gFunctors SI} `{!inG Σ A} (γ : gname) (a : A) : iProp Σ :=
+Local Definition own_def `{SI: indexT} {Σ: gFunctors} `{!inG Σ A} (γ : gname) (a : A) : iProp Σ :=
   uPred_ownM (iRes_singleton γ a).
 Local Definition own_aux : seal (@own_def). by eexists. Qed.
 Definition own := own_aux.(unseal).
@@ -80,7 +80,7 @@ Local Instance: Params (@own) 5 := {}.
 
 (** * Properties about ghost ownership *)
 Section global.
-Context {SI} {Σ: gFunctors SI} `{i : !inG Σ A}.
+Context `{SI: indexT} {Σ: gFunctors} `{i : !inG Σ A}.
 Implicit Types a : A.
 
 Local Lemma inG_unfold_fold (x : inG_apply i (iPrePropO Σ)) :
@@ -201,7 +201,7 @@ Proof. rewrite !own_eq /own_def. apply _. Qed.
 Global Instance own_core_persistent γ a : CoreId a → Persistent (own γ a).
 Proof. rewrite !own_eq /own_def; apply _. Qed.
 
-Lemma later_own `{FiniteIndex SI} γ a : ▷ own γ a -∗ ◇ ∃ b, own γ b ∧ ▷ (a ≡ b).
+Lemma later_own `{!FiniteIndex SI} γ a : ▷ own γ a -∗ ◇ ∃ b, own γ b ∧ ▷ (a ≡ b).
 Proof.
   rewrite own_eq /own_def later_ownM. apply exist_elim=> r.
   assert (NonExpansive (λ r : iResUR Σ, r (inG_id i) !! γ)).
@@ -305,7 +305,7 @@ Global Arguments own_update {_ _ _} [_] _ _ _ _.
 Global Arguments own_update_2 {_ _ _} [_] _ _ _ _ _.
 Global Arguments own_update_3 {_ _ _} [_] _ _ _ _ _ _.
 
-Lemma own_unit {SI} A `{i : !inG Σ (A:ucmra SI)} γ : ⊢ |==> own γ (ε:A).
+Lemma own_unit `{SI: indexT} A `{i : !inG Σ (A:ucmra)} γ : ⊢ |==> own γ (ε:A).
 Proof.
   rewrite /bi_emp_valid (ownM_unit emp) !own_eq /own_def.
   apply bupd_ownM_update, discrete_fun_singleton_update_empty.
@@ -319,7 +319,7 @@ Qed.
 
 (** Big op class instances *)
 Section big_op_instances.
-  Context {SI} {A: ucmra SI} `{!inG Σ A}.
+  Context `{SI: indexT} {A: ucmra} `{!inG Σ A}.
 
   Global Instance own_cmra_sep_homomorphism γ :
     WeakMonoidHomomorphism op uPred_sep (≡) (own γ).
@@ -366,7 +366,7 @@ End big_op_instances.
 
 (** Proofmode class instances *)
 Section proofmode_instances.
-  Context {SI} {Σ: gFunctors SI} `{!inG Σ A}.
+  Context `{SI: indexT} {Σ: gFunctors} `{!inG Σ A}.
   Implicit Types a b : A.
 
   Global Instance into_sep_own γ a b1 b2 :
diff --git a/theories/base_logic/lib/proph_map.v b/theories/base_logic/lib/proph_map.v
index 18f08d9c3cb4f47c38044bcb52baa416da4a9c57..a8e9bee7a0eed2165f62e6e33b566a9f9c59d5a1 100644
--- a/theories/base_logic/lib/proph_map.v
+++ b/theories/base_logic/lib/proph_map.v
@@ -8,25 +8,25 @@ Local Notation proph_map P V := (gmap P (list V)).
 Definition proph_val_list (P V : Type) := list (P * V).
 
 (** The CMRA we need. *)
-Class proph_mapPreG {SI} (P V : Type) (Σ : gFunctors SI) `{Countable P} := {
-  proph_map_preG_inG :> inG Σ (gmap_viewR P (listO $ leibnizO SI V))
+Class proph_mapPreG `{SI: indexT} (P V : Type) (Σ : gFunctors) `{Countable P} := {
+  proph_map_preG_inG :> inG Σ (gmap_viewR P (listO $ leibnizO V))
 }.
 
-Class proph_mapG {SI} (P V : Type) (Σ : gFunctors SI) `{Countable P} := ProphMapG {
+Class proph_mapG `{SI: indexT} (P V : Type) (Σ : gFunctors) `{Countable P} := ProphMapG {
   proph_map_inG :> proph_mapPreG P V Σ;
   proph_map_name : gname
 }.
 Global Arguments proph_map_name {_ _ _ _ _ _} _ : assert.
 
-Definition proph_mapΣ {SI} (P V : Type) `{Countable P} : gFunctors SI :=
-  #[GFunctor (gmap_viewR P (listO $ leibnizO SI V))].
+Definition proph_mapΣ `{SI: indexT} (P V : Type) `{Countable P} : gFunctors :=
+  #[GFunctor (gmap_viewR P (listO $ leibnizO V))].
 
-Global Instance subG_proph_mapPreG {SI} {Σ: gFunctors SI} {P V} `{Countable P} :
+Global Instance subG_proph_mapPreG `{SI: indexT} {Σ: gFunctors} {P V} `{Countable P} :
   subG (proph_mapΣ P V) Σ → proph_mapPreG P V Σ.
 Proof. solve_inG. Qed.
 
 Section definitions.
-  Context {SI} {Σ: gFunctors SI} `{pG : proph_mapG SI P V Σ}.
+  Context `{SI: indexT} {Σ: gFunctors} `{!EqDecision P} `{!Countable P} `{pG : !proph_mapG P V Σ}.
   Implicit Types pvs : proph_val_list P V.
   Implicit Types R : proph_map P V.
   Implicit Types p : P.
@@ -45,10 +45,10 @@ Section definitions.
   Definition proph_map_interp pvs (ps : gset P) : iProp Σ :=
     (∃ R, ⌜proph_resolves_in_list R pvs ∧
           dom R ⊆ ps⌝ ∗
-          own (proph_map_name pG) (gmap_view_auth (V:=listO $ leibnizO SI V) 1 R))%I.
+          own (proph_map_name pG) (gmap_view_auth (V:=listO $ leibnizO V) 1 R))%I.
 
   Definition proph_def (p : P) (vs : list V) : iProp Σ :=
-    own (proph_map_name pG) (gmap_view_frag (V:=listO $ leibnizO SI V) p (DfracOwn 1) vs).
+    own (proph_map_name pG) (gmap_view_frag (V:=listO $ leibnizO V) p (DfracOwn 1) vs).
 
   Definition proph_aux : seal (@proph_def). Proof. by eexists. Qed.
   Definition proph := proph_aux.(unseal).
@@ -77,7 +77,7 @@ End list_resolves.
 The key difference to [proph_map_init] is that the [inG] instances in the new
 [proph_mapPreG] instance are related to the original [proph_mapPreG] instance,
 whereas [proph_map_init] forgets about that relation. *)
-Lemma proph_map_init_names {SI: indexT} {Σ: gFunctors SI} `{Countable P, !proph_mapPreG P V Σ} pvs ps :
+Lemma proph_map_init_names `{SI: indexT} {Σ: gFunctors} `{Countable P, !proph_mapPreG P V Σ} pvs ps :
   ⊢ |==> ∃ γ, let H := ProphMapG SI P V Σ _ _ _ γ in proph_map_interp pvs ps.
 Proof.
   iMod (own_alloc (gmap_view_auth 1 ∅)) as (γ) "Hh".
@@ -86,7 +86,7 @@ Proof.
   iPureIntro. done.
 Qed.
 
-Lemma proph_map_init {SI: indexT} {Σ: gFunctors SI} `{Countable P, !proph_mapPreG P V Σ} pvs ps :
+Lemma proph_map_init `{SI: indexT} {Σ: gFunctors} `{Countable P, !proph_mapPreG P V Σ} pvs ps :
   ⊢ |==> ∃ _ : proph_mapG P V Σ, proph_map_interp pvs ps.
 Proof.
   iMod (proph_map_init_names pvs ps) as (γ) "H". iModIntro.
@@ -94,7 +94,7 @@ Proof.
 Qed.
 
 Section proph_map.
-  Context {SI} {Σ: gFunctors SI} `{proph_mapG SI P V Σ}.
+  Context `{SI: indexT} {Σ: gFunctors}  `{!EqDecision P} `{!Countable P} `{!proph_mapG P V Σ}.
   Implicit Types p : P.
   Implicit Types v : V.
   Implicit Types vs : list V.
diff --git a/theories/base_logic/lib/satisfiable.v b/theories/base_logic/lib/satisfiable.v
index 8fe85187f5b2f1af89fa4831715995cb888ca9d8..5d7b1696c7c8ba4b107540c22cb025510a57b3c8 100644
--- a/theories/base_logic/lib/satisfiable.v
+++ b/theories/base_logic/lib/satisfiable.v
@@ -8,7 +8,7 @@ Import uPred.
 
 
 (* we first lift satisfiability from uPred to iProp *)
-Definition iProp_sat_def {SI: indexT} {Σ: gFunctors SI} := @uPred_primitive.uPred_sat SI (iResUR Σ).
+Definition iProp_sat_def `{SI: indexT} {Σ: gFunctors} := @uPred_primitive.uPred_sat SI (iResUR Σ).
 Local Definition iProp_sat_aux : seal (@iProp_sat_def). Proof. by eexists. Qed.
 Definition iProp_sat := iProp_sat_aux.(unseal).
 Global Arguments iProp_sat {SI Σ} P.
@@ -16,7 +16,7 @@ Local Definition iProp_sat_eq : @iProp_sat = @iProp_sat_def := iProp_sat_aux.(se
 Local Instance: Params (@iProp_sat) 2 := {}.
 
 Section iProp_sat.
-  Context {SI} {Σ: gFunctors SI}.
+  Context `{SI: indexT} {Σ: gFunctors}.
 
   Global Instance iProp_sat_instance: Satisfiable (@iProp_sat SI Σ).
   Proof. rewrite iProp_sat_eq /iProp_sat_def; apply _. Qed.
@@ -42,25 +42,25 @@ End iProp_sat.
 
 (* We develop a validity judgement where we can explicitly control
    the ghost names that are allocated *)
-Definition alloc_names_def {SI} {Σ: gFunctors SI} (G: gset gname) (P: iProp Σ): Prop :=
+Definition alloc_names_def `{SI: indexT} {Σ: gFunctors} (G: gset gname) (P: iProp Σ): Prop :=
   (∃ m: iResUR Σ, ✓ m ∧ (∀ i, dom (m i) ⊆ G) ∧ (uPred_ownM m ⊢ P)).
 Definition alloc_names_aux : seal (@alloc_names_def). by eexists. Qed.
 Definition alloc_names := alloc_names_aux.(unseal).
 Arguments alloc_names {SI Σ} _ _.
 Definition alloc_names_eq : @alloc_names = @alloc_names_def := alloc_names_aux.(seal_eq).
-Instance: Params (@alloc_names) 4 := {}.
+Global Instance: Params (@alloc_names) 4 := {}.
 
 (* we hide the names *)
-Definition alloc {SI} {Σ: gFunctors SI} (P: iProp Σ) := ∃ G, alloc_names G P.
+Definition alloc `{SI: indexT} {Σ: gFunctors} (P: iProp Σ) := ∃ G, alloc_names G P.
 
-Class Alloc {SI} {Σ: gFunctors SI} (X: Type) (Φ: X → iProp Σ) (φ: Type):=
+Class Alloc `{SI: indexT} {Σ: gFunctors} (X: Type) (Φ: X → iProp Σ) (φ: Type):=
   can_alloc: ∀ P, φ → alloc P → ∃ x: X, alloc (P ∗ Φ x).
 
 Global Hint Mode Alloc - - + ! - : typeclass_instances.
 Global Arguments can_alloc {SI Σ X} Φ {φ _ _} _ _.
 
 Section alloc.
-  Context {SI} {Σ: gFunctors SI}.
+  Context `{SI: indexT} {Σ: gFunctors}.
 
   Lemma alloc_names_empty : alloc_names ∅ (True%I: iProp Σ).
   Proof.
@@ -133,7 +133,7 @@ Section alloc.
   Qed.
 
   (* derived *)
-  Lemma alloc_names_own_fresh G (P: iProp Σ) {A: cmra SI} (a: A) `{!inG Σ A}:
+  Lemma alloc_names_own_fresh G (P: iProp Σ) {A: cmra} (a: A) `{!inG Σ A}:
     alloc_names G P → ✓ a → ∃ γ, alloc_names (G ∪ {[γ]}) (P ∗ own γ a).
   Proof.
     intros Halloc Hv. exists (fresh G).
@@ -148,7 +148,7 @@ Section alloc.
     exists ∅. apply alloc_names_empty.
   Qed.
 
-  Lemma alloc_fresh_res {A: cmra SI} `{!inG Σ A} (a: A) P:
+  Lemma alloc_fresh_res {A: cmra} `{!inG Σ A} (a: A) P:
     ✓ a → alloc P → ∃ γ, alloc (P ∗ own γ a).
   Proof.
     intros Hv [G Halloc].
@@ -176,7 +176,7 @@ Section alloc.
   Proof. intros [G ?]; by eapply alloc_names_iProp_sat. Qed.
 
   (* this instance can be used to allocate some ghost state *)
-  Global Instance alloc_gname_inst {A: cmra SI} `{!inG Σ A} (a: A):
+  Global Instance alloc_gname_inst {A: cmra} `{!inG Σ A} (a: A):
     Alloc gname (λ γ, own γ a) (✓ a).
   Proof.
     intros ???; by eapply alloc_fresh_res.
@@ -203,11 +203,11 @@ End alloc.
 
 
 (* we create a notion of satisfiability which includes invariant masks *)
-Class SatisfiableAtFupd {SI} {Σ: gFunctors SI} `{!invG Σ} (sat_at: coPset → iProp Σ → Prop) := {
+Class SatisfiableAtFupd `{SI: indexT} {Σ: gFunctors} `{!invG Σ} (sat_at: coPset → iProp Σ → Prop) := {
   sat_fupd E1 E2 P: sat_at E1 (|={E1, E2}=> P)%I → sat_at E2 P
 }.
 
-Class SatisfiableAt {SI} {Σ: gFunctors SI} `{!invG Σ} (sat_at: coPset → iProp Σ → Prop) := {
+Class SatisfiableAt `{SI: indexT} {Σ: gFunctors} `{!invG Σ} (sat_at: coPset → iProp Σ → Prop) := {
   sat_at_satisfiable E:> Satisfiable (sat_at E);
   sat_at_bupd E:> SatisfiableBUpd (sat_at E);
   sat_at_later E:> SatisfiableLater (sat_at E);
@@ -218,7 +218,7 @@ Notation SatisfiableAtExists X sat_at := (∀ E, SatisfiableExists X (sat_at E))
 
 (* there is a canonical satisfiability instance for every notion of satisfiable *)
 Section canonical_sat_at.
-  Context {SI} {Σ: gFunctors SI} `{!invG Σ} {sat: iProp Σ → Prop} `{!Satisfiable sat} `{!SatisfiableBUpd sat} `{!SatisfiableLater sat}.
+  Context `{SI: indexT} {Σ: gFunctors} `{!invG Σ} {sat: iProp Σ → Prop} `{!Satisfiable sat} `{!SatisfiableBUpd sat} `{!SatisfiableLater sat}.
 
   Definition sat_at E := (sat_frame (sat := sat) (wsat ∗ ownE E)%I).
 
@@ -244,7 +244,7 @@ Notation iProp_sat_at := (sat_at (sat := iProp_sat)).
 
 (* framing preserves SatisfiableAtFUpd *)
 Section sat_at_frame.
-  Context {SI} {Σ: gFunctors SI} `{!invG Σ} {sat_at: coPset → iProp Σ → Prop}.
+  Context `{SI: indexT} {Σ: gFunctors} `{!invG Σ} {sat_at: coPset → iProp Σ → Prop}.
 
   Definition sat_at_frame F E P := sat_frame (sat := sat_at E) F P.
 
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index 30e7975e32a0a4dab5e504b6d1f70bc53bd30a7b..8406b13d31ea78b2a595f0e3a329bc0027947385 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -8,25 +8,25 @@ Import uPred.
 (* "Saved anything" -- this can give you saved propositions, saved predicates,
    saved whatever-you-like. *)
 
-Class savedAnythingG {SI : indexT} (Σ : gFunctors SI) (F : oFunctor SI) := SavedAnythingG {
+Class savedAnythingG `{SI : indexT} (Σ : gFunctors) (F : oFunctor) := SavedAnythingG {
   saved_anything_inG :> inG Σ (agreeR (oFunctor_apply F (iPropO Σ)));
   saved_anything_contractive : oFunctorContractive F (* NOT an instance to avoid cycles with [subG_savedAnythingΣ]. *)
 }.
-Definition savedAnythingΣ {SI : indexT} (F : oFunctor SI) `{!oFunctorContractive F} : gFunctors SI :=
+Definition savedAnythingΣ `{SI : indexT} (F : oFunctor) `{!oFunctorContractive F} : gFunctors :=
   #[ GFunctor (agreeRF F) ].
 
-Global Instance subG_savedAnythingΣ {SI Σ} {F : oFunctor SI} `{!oFunctorContractive F} :
+Global Instance subG_savedAnythingΣ `{SI : indexT} {Σ} {F : oFunctor} `{!oFunctorContractive F} :
   subG (savedAnythingΣ F) Σ → savedAnythingG Σ F.
 Proof. solve_inG. Qed.
 
-Definition saved_anything_own {SI} {Σ: gFunctors SI} {F} `{!savedAnythingG Σ F}
+Definition saved_anything_own `{SI : indexT} {Σ: gFunctors} {F} `{!savedAnythingG Σ F}
     (γ : gname) (x : oFunctor_apply F (iPropO Σ)) : iProp Σ :=
   own γ (to_agree x).
-Typeclasses Opaque saved_anything_own.
+Global Typeclasses Opaque saved_anything_own.
 Global Instance: Params (@saved_anything_own) 5 := {}.
 
 Section saved_anything.
-  Context {SI} {Σ: gFunctors SI} {F} `{!savedAnythingG Σ F}.
+  Context `{SI : indexT} {Σ: gFunctors} {F} `{!savedAnythingG Σ F}.
   Implicit Types x y : oFunctor_apply F (iPropO Σ).
   Implicit Types γ : gname.
 
@@ -66,27 +66,27 @@ End saved_anything.
 Notation savedPropG Σ := (savedAnythingG Σ (▶ (∙ _))).
 Notation savedPropΣ := (savedAnythingΣ (▶ (∙ _))).
 
-Definition saved_prop_own {SI} {Σ : gFunctors SI} `{!savedPropG Σ} (γ : gname) (P: iProp Σ) :=
+Definition saved_prop_own `{SI : indexT} {Σ : gFunctors} `{!savedPropG Σ} (γ : gname) (P: iProp Σ) :=
   saved_anything_own (F := ▶ (∙ _)) γ (Next P).
 
-Instance saved_prop_own_contractive {SI} {Σ : gFunctors SI} `{!savedPropG Σ} γ :
+Global Instance saved_prop_own_contractive `{SI : indexT} {Σ : gFunctors} `{!savedPropG Σ} γ :
   Contractive (saved_prop_own γ).
 Proof. solve_contractive. Qed.
 
-Lemma saved_prop_alloc_strong {SI} {Σ : gFunctors SI} `{!savedPropG Σ} (I : gname → Prop) (P: iProp Σ) :
+Lemma saved_prop_alloc_strong `{SI : indexT} {Σ : gFunctors} `{!savedPropG Σ} (I : gname → Prop) (P: iProp Σ) :
   pred_infinite I →
   ⊢ |==> ∃ γ, ⌜I γ⌝ ∗ saved_prop_own γ P.
 Proof. iIntros (?). by iApply saved_anything_alloc_strong. Qed.
 
-Lemma saved_prop_alloc_cofinite {SI} {Σ : gFunctors SI} `{!savedPropG Σ} (G : gset gname) (P: iProp Σ) :
+Lemma saved_prop_alloc_cofinite `{SI : indexT} {Σ : gFunctors} `{!savedPropG Σ} (G : gset gname) (P: iProp Σ) :
   ⊢ |==> ∃ γ, ⌜γ ∉ G⌝ ∗ saved_prop_own γ P.
 Proof. iApply saved_anything_alloc_cofinite. Qed.
 
-Lemma saved_prop_alloc `{Σ : gFunctors SI} `{!savedPropG Σ} (P: iProp Σ) :
+Lemma saved_prop_alloc `{SI : indexT} {Σ : gFunctors} `{!savedPropG Σ} (P: iProp Σ) :
   ⊢ |==> ∃ γ, saved_prop_own γ P.
 Proof. iApply saved_anything_alloc. Qed.
 
-Lemma saved_prop_agree `{Σ : gFunctors SI} `{!savedPropG Σ} γ P Q :
+Lemma saved_prop_agree `{SI : indexT} {Σ : gFunctors} `{!savedPropG Σ} γ P Q :
   saved_prop_own γ P -∗ saved_prop_own γ Q -∗ ▷ (P ≡ Q).
 Proof.
   iIntros "HP HQ". iApply later_equivI.
@@ -97,10 +97,10 @@ Qed.
 Notation savedPredG Σ A := (savedAnythingG Σ (A -d> ▶ (∙ _))).
 Notation savedPredΣ A := (savedAnythingΣ (A -d> ▶ (∙ _))).
 
-Definition saved_pred_own `{Σ : gFunctors SI} `{!savedPredG Σ A} (γ : gname) (Φ : A → iProp Σ) :=
+Definition saved_pred_own `{SI : indexT} {Σ : gFunctors} `{!savedPredG Σ A} (γ : gname) (Φ : A → iProp Σ) :=
   saved_anything_own (F := A -d> ▶ (∙ _)) γ (OfeMor Next ∘ Φ).
 
-Global Instance saved_pred_own_contractive `{Σ : gFunctors SI} `{!savedPredG Σ A} γ :
+Global Instance saved_pred_own_contractive `{SI : indexT} {Σ : gFunctors} `{!savedPredG Σ A} γ :
   Contractive (saved_pred_own γ : (A -d> iPropO Σ) → iProp Σ).
 Proof.
   (* TODO: fix this once f_contractive is fixed *)
@@ -109,21 +109,21 @@ Proof.
   intros ??. by apply H.
 Qed.
 
-Lemma saved_pred_alloc_strong `{Σ : gFunctors SI} `{!savedPredG Σ A} (I : gname → Prop) (Φ : A → iProp Σ) :
+Lemma saved_pred_alloc_strong `{SI : indexT} {Σ : gFunctors} `{!savedPredG Σ A} (I : gname → Prop) (Φ : A → iProp Σ) :
   pred_infinite I →
   ⊢ |==> ∃ γ, ⌜I γ⌝ ∗ saved_pred_own γ Φ.
 Proof. iIntros (?). by iApply saved_anything_alloc_strong. Qed.
 
-Lemma saved_pred_alloc_cofinite `{Σ : gFunctors SI} `{!savedPredG Σ A} (G : gset gname) (Φ : A → iProp Σ) :
+Lemma saved_pred_alloc_cofinite `{SI : indexT} {Σ : gFunctors} `{!savedPredG Σ A} (G : gset gname) (Φ : A → iProp Σ) :
   ⊢ |==> ∃ γ, ⌜γ ∉ G⌝ ∗ saved_pred_own γ Φ.
 Proof. iApply saved_anything_alloc_cofinite. Qed.
 
-Lemma saved_pred_alloc `{Σ : gFunctors SI} `{!savedPredG Σ A} (Φ : A → iProp Σ) :
+Lemma saved_pred_alloc `{SI : indexT} {Σ : gFunctors} `{!savedPredG Σ A} (Φ : A → iProp Σ) :
   ⊢ |==> ∃ γ, saved_pred_own γ Φ.
 Proof. iApply saved_anything_alloc. Qed.
 
 (* We put the `x` on the outside to make this lemma easier to apply. *)
-Lemma saved_pred_agree `{Σ : gFunctors SI} `{!savedPredG Σ A} γ Φ Ψ x :
+Lemma saved_pred_agree `{SI : indexT} {Σ : gFunctors} `{!savedPredG Σ A} γ Φ Ψ x :
   saved_pred_own γ Φ -∗ saved_pred_own γ Ψ -∗ ▷ (Φ x ≡ Ψ x).
 Proof.
   unfold saved_pred_own. iIntros "#HΦ #HΨ /=". iApply later_equivI.
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index 55ba24a5243ea5667ff9f44dfeb63d96719b2442..ba2c8959355f358fad0670e2b2acc63bad2cd946 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -8,55 +8,55 @@ From iris.prelude Require Import options.
 exception of what's in the [invG] module. The module [invG] is thus exported in
 [fancy_updates], which [wsat] is only imported. *)
 Module invG.
-  Class invPreG {SI} (Σ : gFunctors SI) : Set := WsatPreG {
+  Class invPreG `{SI : indexT} (Σ : gFunctors) : Set := WsatPreG {
     inv_inPreG :> inG Σ (gmap_viewR positive (laterO (iPropO Σ)));
-    enabled_inPreG :> inG Σ (coPset_disjR SI);
+    enabled_inPreG :> inG Σ (coPset_disjR);
     disabled_inPreG :> inG Σ (gset_disjR positive);
   }.
 
-  Class invG {SI} (Σ : gFunctors SI) : Set := InvG {
+  Class invG `{SI : indexT} (Σ : gFunctors) : Set := InvG {
     inv_inG :> invPreG Σ;
     invariant_name : gname;
     enabled_name : gname;
     disabled_name : gname;
   }.
 
-  Definition invΣ (SI: indexT) : gFunctors SI :=
-    #[GFunctor (gmap_viewRF positive (laterOF (idOF SI)));
-      GFunctor (coPset_disjR SI);
+  Definition invΣ `{SI : indexT} : gFunctors :=
+    #[GFunctor (gmap_viewRF positive (laterOF idOF));
+      GFunctor (coPset_disjR);
       GFunctor (gset_disjR positive)].
 
-  Global Instance subG_invΣ {SI} {Σ: gFunctors SI} : subG (invΣ SI) Σ → invPreG Σ.
+  Global Instance subG_invΣ `{SI : indexT} {Σ: gFunctors} : subG (invΣ) Σ → invPreG Σ.
   Proof. solve_inG. Qed.
 End invG.
 Import invG.
 
-Definition invariant_unfold {SI} {Σ: gFunctors SI} (P : iProp Σ) : later (iProp Σ) :=
+Definition invariant_unfold `{SI : indexT} {Σ: gFunctors} (P : iProp Σ) : later (iProp Σ) :=
   Next P.
-Definition ownI {SI} {Σ: gFunctors SI} `{!invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
+Definition ownI `{SI : indexT} {Σ: gFunctors} `{!invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
   own invariant_name (gmap_view_frag i DfracDiscarded (invariant_unfold P)).
 Global Arguments ownI {_ _ _} _ _%I.
-Typeclasses Opaque ownI.
+Global Typeclasses Opaque ownI.
 Global Instance: Params (@invariant_unfold) 2 := {}.
 Global Instance: Params (@ownI) 4 := {}.
 
-Definition ownE {SI} {Σ: gFunctors SI} `{!invG Σ} (E : coPset) : iProp Σ :=
+Definition ownE `{SI : indexT} {Σ: gFunctors} `{!invG Σ} (E : coPset) : iProp Σ :=
   own enabled_name (CoPset E).
-Typeclasses Opaque ownE.
+Global Typeclasses Opaque ownE.
 Global Instance: Params (@ownE) 4 := {}.
 
-Definition ownD {SI} {Σ: gFunctors SI} `{!invG Σ} (E : gset positive) : iProp Σ :=
+Definition ownD `{SI : indexT} {Σ: gFunctors} `{!invG Σ} (E : gset positive) : iProp Σ :=
   own disabled_name (GSet E).
-Typeclasses Opaque ownD.
+Global Typeclasses Opaque ownD.
 Global Instance: Params (@ownD) 4 := {}.
 
-Definition wsat {SI} {Σ: gFunctors SI} `{!invG Σ} : iProp Σ :=
+Definition wsat `{SI : indexT} {Σ: gFunctors} `{!invG Σ} : iProp Σ :=
   locked (∃ I : gmap positive (iProp Σ),
     own invariant_name (gmap_view_auth 1 (invariant_unfold <$> I)) ∗
     [∗ map] i ↦ Q ∈ I, ▷ Q ∗ ownD {[i]} ∨ ownE {[i]})%I.
 
 Section wsat.
-Context {SI} {Σ: gFunctors SI} `{!invG Σ}.
+Context `{SI : indexT} {Σ: gFunctors} `{!invG Σ}.
 Implicit Types P : iProp Σ.
 
 (* Invariants *)
@@ -70,7 +70,7 @@ Proof. rewrite /ownI. apply _. Qed.
 Lemma ownE_empty : ⊢ |==> ownE ∅.
 Proof.
   rewrite /bi_emp_valid.
-  by rewrite (own_unit (coPset_disjUR SI) enabled_name).
+  by rewrite (own_unit coPset_disjUR enabled_name).
 Qed.
 Lemma ownE_op E1 E2 : E1 ## E2 → ownE (E1 ∪ E2) ⊣⊢ ownE E1 ∗ ownE E2.
 Proof. intros. by rewrite /ownE -own_op coPset_disj_union. Qed.
@@ -183,7 +183,7 @@ Qed.
 End wsat.
 
 (* Allocation of an initial wolibrld *)
-Lemma wsat_alloc_strong {SI: indexT} {Σ: gFunctors SI} `{!invPreG Σ} :
+Lemma wsat_alloc_strong {SI: indexT} {Σ: gFunctors} `{!invPreG Σ} :
   ⊢ |==> ∃ γI γE γD : gname, let H := InvG _ _ _ γI γE γD in wsat ∗ ownE ⊤.
 Proof.
   iIntros.
@@ -197,7 +197,7 @@ Proof.
 Qed.
 
 
-Lemma wsat_alloc {SI: indexT} {Σ: gFunctors SI} `{!invPreG Σ} :
+Lemma wsat_alloc {SI: indexT} {Σ: gFunctors} `{!invPreG Σ} :
   bi_emp_valid (|==> ∃ _ : invG Σ, wsat ∗ ownE ⊤)%I.
 Proof.
   iIntros. iMod wsat_alloc_strong as (γI γE γD) "H". iModIntro.
diff --git a/theories/base_logic/proofmode.v b/theories/base_logic/proofmode.v
index a36fa1d1b95c72685915c59ccc95dc441ee0123e..b6eca5ef84e07e83434da7a615beaad4e0157391 100644
--- a/theories/base_logic/proofmode.v
+++ b/theories/base_logic/proofmode.v
@@ -7,14 +7,14 @@ Import base_logic.bi.uPred.
 
 (* Setup of the proof mode *)
 Section class_instances.
-Context {SI} {M : ucmra SI}.
+Context `{SI: indexT} {M : ucmra}.
 Implicit Types P Q R : uPred M.
 
 Global Instance into_pure_cmra_valid `{!CmraDiscrete A} (a : A) :
   @IntoPure SI (uPredI M) (✓ a) (✓ a).
 Proof. by rewrite /IntoPure discrete_valid. Qed.
 
-Global Instance from_pure_cmra_valid {A : cmra SI} (a : A) :
+Global Instance from_pure_cmra_valid {A : cmra} (a : A) :
   @FromPure SI (uPredI M) false (✓ a) (✓ a).
 Proof.
   rewrite /FromPure /=. eapply bi.pure_elim=> // ?.
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index d95a2177ceacc3ab92332d5103a769d547e128a0..afa5f6f324e04236c1ecbfebeb2dd1b9159d0f02 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -102,8 +102,8 @@ This completes the proof.
 
 *)
 
-Record uPred {SI: indexT} (M : ucmra SI) : Type := UPred {
-  uPred_holds : SI → M → Prop;
+Record uPred `{SI: indexT} (M : ucmra) : Type := UPred {
+  uPred_holds : index → M → Prop;
 
   uPred_mono n1 n2 x1 x2 :
     uPred_holds n1 x1 → x1 ≼{n2} x2 → n2 ⪯ n1 → uPred_holds n2 x2
@@ -118,15 +118,15 @@ Add Printing Constructor uPred.
 Global Instance: Params (@uPred_holds) 4 := {}.
 
 Section cofe.
-  Context {SI: indexT} {M : ucmra SI}.
+  Context `{SI: indexT} {M : ucmra}.
 
   Inductive uPred_equiv' (P Q : uPred M) : Prop :=
     { uPred_in_equiv : ∀ n x, ✓{n} x → P n x ↔ Q n x }.
   Local Instance uPred_equiv : Equiv (uPred M) := uPred_equiv'.
-  Inductive uPred_dist' (n : SI) (P Q : uPred M) : Prop :=
+  Inductive uPred_dist' (n : index) (P Q : uPred M) : Prop :=
     { uPred_in_dist : ∀ n' x, n' ⪯ n → ✓{n'} x → P n' x ↔ Q n' x }.
-  Local Instance uPred_dist : Dist SI (uPred M) := uPred_dist'.
-  Definition uPred_ofe_mixin : OfeMixin SI (uPred M).
+  Local Instance uPred_dist : Dist (uPred M) := uPred_dist'.
+  Definition uPred_ofe_mixin : OfeMixin (uPred M).
   Proof.
     split.
     - intros P Q; split.
@@ -137,10 +137,10 @@ Section cofe.
       + by intros P Q HPQ; split=> x i ??; symmetry; apply HPQ.
       + intros P Q Q' HP HQ; split=> i x ??.
         by trans (Q i x);[apply HP|apply HQ].
-    - intros α β P Q HPQ Hpre; split=> i x ??; apply HPQ; last by eauto. 
+    - intros α β P Q HPQ Hpre; split=> i x ??; apply HPQ; last by eauto.
       right; eapply index_le_lt_trans; eauto.
   Qed.
-  Canonical Structure uPredO : ofe SI := Ofe (uPred M) uPred_ofe_mixin.
+  Canonical Structure uPredO : ofe := Ofe (uPred M) uPred_ofe_mixin.
 
   Program Definition uPred_compl : chain uPredO → uPredO := λ c,
     {| uPred_holds n x := ∀ n', n' ⪯ n → ✓{n'} x → c n' n' x |}.
@@ -159,8 +159,8 @@ Section cofe.
     - eapply cmra_includedN_le=>//; eauto with index.
     - done.
   Qed.
-  Lemma uPred_bcompl'_ne α (c d : bchain uPredO α) (β : SI): 
-    (∀ (γ : SI) (Hγ : γ ≺ α), c γ Hγ ≡{β}≡ d γ Hγ) → 
+  Lemma uPred_bcompl'_ne α (c d : bchain uPredO α) (β : index):
+    (∀ (γ : index) (Hγ : γ ≺ α), c γ Hγ ≡{β}≡ d γ Hγ) →
     uPred_bcompl' α c ≡{β}≡ uPred_bcompl' α d.
   Proof.
     intros Hne; split=> i x Hiβ Hv; split.
@@ -180,7 +180,7 @@ Section cofe.
   Next Obligation.
     intros α Hα c; split=>i x Hiα Hv.
     etrans; [|unshelve by symmetry; apply (bchain_cauchy α c)]; last by eapply index_le_lt_trans; eauto.
-    split=>H'; [by apply H'|]. intros n' Hn' Hin' H. 
+    split=>H'; [by apply H'|]. intros n' Hn' Hin' H.
     unshelve eapply (bchain_cauchy α c n' i); [by eauto using index_le_lt_trans | by eauto | by eauto | by eauto | ].
     by eapply uPred_mono.
   Qed.
@@ -196,7 +196,7 @@ Section cofe.
 
   Global Program Instance truncatable : ProtoTruncatable uPredO :=
   {
-    proto_trunc α := λne a, uPred_bcompl' (index_succ _ α) (bchain_const a (index_succ _ α)  );
+    proto_trunc α := λne a, uPred_bcompl' (index_succ α) (bchain_const a (index_succ α)  );
   }.
   Next Obligation.
     intros α α' x y Heq. by apply uPred_bcompl'_ne.
@@ -220,21 +220,21 @@ Section cofe.
 End cofe.
 Global Arguments uPredO {_} _.
 
-Global Instance uPred_ne {SI} {M: ucmra SI} (P : uPred M) n : Proper (dist n ==> iff) (P n).
+Global Instance uPred_ne `{SI: indexT} {M: ucmra} (P : uPred M) n : Proper (dist n ==> iff) (P n).
 Proof.
   intros x1 x2 Hx; split=> ?; eapply uPred_mono; eauto; by rewrite Hx.
 Qed.
-Global Instance uPred_proper {SI} {M: ucmra SI} (P : uPred M) n : Proper ((≡) ==> iff) (P n).
+Global Instance uPred_proper `{SI: indexT} {M: ucmra} (P : uPred M) n : Proper ((≡) ==> iff) (P n).
 Proof. by intros x1 x2 Hx; apply uPred_ne, equiv_dist. Qed.
 
-Lemma uPred_holds_ne {SI} {M: ucmra SI} (P Q : uPred M) n1 n2 x :
+Lemma uPred_holds_ne `{SI: indexT} {M: ucmra} (P Q : uPred M) n1 n2 x :
   P ≡{n2}≡ Q → n2 ⪯ n1 → ✓{n2} x → Q n1 x → P n2 x.
 Proof.
   intros [Hne] ???. eapply Hne; try done. eauto using uPred_mono, cmra_validN_le.
 Qed.
 
 (* Equivalence to the definition of uPred in the appendix. *)
-Lemma uPred_alt {SI: indexT} {M : ucmra SI} (P: SI → M → Prop) :
+Lemma uPred_alt `{SI: indexT} {M : ucmra} (P: index → M → Prop) :
   (∀ n1 n2 x1 x2, P n1 x1 → x1 ≼{n1} x2 → n2 ⪯ n1 → P n2 x2) ↔
   ( (∀ x n1 n2, n2 ⪯ n1 → P n1 x → P n2 x) (* Pointwise down-closed *)
   ∧ (∀ n x1 x2, x1 ≡{n}≡ x2 → ∀ m, m ⪯ n → P m x1 ↔ P m x2) (* Non-expansive *)
@@ -251,30 +251,30 @@ Proof.
 Qed.
 
 (** functor *)
-Program Definition uPred_map {SI: indexT} {M1 M2 : ucmra SI} (f : M2 -n> M1)
+Program Definition uPred_map `{SI: indexT} {M1 M2 : ucmra} (f : M2 -n> M1)
   `{!CmraMorphism f} (P : uPred M1) :
   uPred M2 := {| uPred_holds n x := P n (f x) |}.
 Next Obligation. naive_solver eauto using uPred_mono, cmra_morphism_monotoneN. Qed.
 
-Global Instance uPred_map_ne {SI: indexT} {M1 M2 : ucmra SI} (f : M2 -n> M1)
+Global Instance uPred_map_ne `{SI: indexT} {M1 M2 : ucmra} (f : M2 -n> M1)
   `{!CmraMorphism f} n : Proper (dist n ==> dist n) (uPred_map f).
 Proof.
   intros x1 x2 Hx; split=> n' y ??.
   split; apply Hx; auto using cmra_morphism_validN.
 Qed.
-Lemma uPred_map_id {SI} {M : ucmra SI} (P : uPred M): uPred_map cid P ≡ P.
+Lemma uPred_map_id `{SI: indexT} {M : ucmra} (P : uPred M): uPred_map cid P ≡ P.
 Proof. by split=> n x ?. Qed.
-Lemma uPred_map_compose {SI} {M1 M2 M3 : ucmra SI} (f : M1 -n> M2) (g : M2 -n> M3)
+Lemma uPred_map_compose `{SI: indexT} {M1 M2 M3 : ucmra} (f : M1 -n> M2) (g : M2 -n> M3)
     `{!CmraMorphism f, !CmraMorphism g} (P : uPred M3):
   uPred_map (g ◎ f) P ≡ uPred_map f (uPred_map g P).
 Proof. by split=> n x Hx. Qed.
-Lemma uPred_map_ext {SI} {M1 M2 : ucmra SI} (f g : M1 -n> M2)
+Lemma uPred_map_ext `{SI: indexT} {M1 M2 : ucmra} (f g : M1 -n> M2)
       `{!CmraMorphism f} `{!CmraMorphism g}:
   (∀ x, f x ≡ g x) → ∀ x, uPred_map f x ≡ uPred_map g x.
 Proof. intros Hf P; split=> n x Hx /=; by rewrite /uPred_holds /= Hf. Qed.
-Definition uPredO_map {SI} {M1 M2 : ucmra SI} (f : M2 -n> M1) `{!CmraMorphism f} :
+Definition uPredO_map `{SI: indexT} {M1 M2 : ucmra} (f : M2 -n> M1) `{!CmraMorphism f} :
   uPredO M1 -n> uPredO M2 := OfeMor (uPred_map f : uPredO M1 → uPredO M2).
-Lemma uPredO_map_ne {SI} {M1 M2 : ucmra SI} (f g : M2 -n> M1)
+Lemma uPredO_map_ne `{SI: indexT} {M1 M2 : ucmra} (f g : M2 -n> M1)
     `{!CmraMorphism f, !CmraMorphism g} n :
   f ≡{n}≡ g → uPredO_map f ≡{n}≡ uPredO_map g.
 Proof.
@@ -282,7 +282,7 @@ Proof.
     rewrite /uPred_holds /= (dist_le _ _ _ _(Hfg y)).
 Qed.
 
-Program Definition uPredOF {SI} (F : urFunctor SI) : oFunctor SI := {|
+Program Definition uPredOF `{SI: indexT} (F : urFunctor) : oFunctor := {|
   oFunctor_car A B := uPredO (urFunctor_car F B A);
   oFunctor_map A1 A2 B1 B2 fg := uPredO_map (urFunctor_map F (fg.2, fg.1))
 |}.
@@ -299,7 +299,7 @@ Next Obligation.
   apply uPred_map_ext=>y; apply urFunctor_map_compose.
 Qed.
 
-Instance uPredOF_contractive {SI} (F: urFunctor SI) :
+Global Instance uPredOF_contractive `{SI: indexT} (F: urFunctor) :
   urFunctorContractive F → oFunctorContractive (uPredOF F).
 Proof.
   intros ? A1 A2 B1 B2 n P Q HPQ. apply uPredO_map_ne, urFunctor_map_contractive.
@@ -307,12 +307,12 @@ Proof.
 Qed.
 
 (** logical entailement *)
-Inductive uPred_entails {SI} {M: ucmra SI} (P Q : uPred M) : Prop :=
+Inductive uPred_entails `{SI: indexT} {M: ucmra} (P Q : uPred M) : Prop :=
   { uPred_in_entails : ∀ n x, ✓{n} x → P n x → Q n x }.
 Global Hint Resolve uPred_mono : uPred_def.
 
 (** logical connectives *)
-Program Definition uPred_pure_def {SI} {M: ucmra SI} (φ : Prop) : uPred M :=
+Program Definition uPred_pure_def `{SI: indexT} {M: ucmra} (φ : Prop) : uPred M :=
   {| uPred_holds n x := φ |}.
 Solve Obligations with done.
 Definition uPred_pure_aux : seal (@uPred_pure_def). Proof. by eexists. Qed.
@@ -321,7 +321,7 @@ Global Arguments uPred_pure {SI M}.
 Definition uPred_pure_eq :
   @uPred_pure = @uPred_pure_def := uPred_pure_aux.(seal_eq).
 
-Program Definition uPred_and_def {SI} {M: ucmra SI} (P Q : uPred M) : uPred M :=
+Program Definition uPred_and_def `{SI: indexT} {M: ucmra} (P Q : uPred M) : uPred M :=
   {| uPred_holds n x := P n x ∧ Q n x |}.
 Solve Obligations with naive_solver eauto 2 with uPred_def.
 Definition uPred_and_aux : seal (@uPred_and_def). Proof. by eexists. Qed.
@@ -329,7 +329,7 @@ Definition uPred_and := uPred_and_aux.(unseal).
 Global Arguments uPred_and {SI M}.
 Definition uPred_and_eq: @uPred_and = @uPred_and_def := uPred_and_aux.(seal_eq).
 
-Program Definition uPred_or_def {SI} {M: ucmra SI} (P Q : uPred M) : uPred M :=
+Program Definition uPred_or_def `{SI: indexT} {M: ucmra} (P Q : uPred M) : uPred M :=
   {| uPred_holds n x := P n x ∨ Q n x |}.
 Solve Obligations with naive_solver eauto 2 with uPred_def.
 Definition uPred_or_aux : seal (@uPred_or_def). Proof. by eexists. Qed.
@@ -337,7 +337,7 @@ Definition uPred_or := uPred_or_aux.(unseal).
 Global Arguments uPred_or {SI M}.
 Definition uPred_or_eq: @uPred_or = @uPred_or_def := uPred_or_aux.(seal_eq).
 
-Program Definition uPred_impl_def {SI} {M: ucmra SI} (P Q : uPred M) : uPred M :=
+Program Definition uPred_impl_def `{SI: indexT} {M: ucmra} (P Q : uPred M) : uPred M :=
   {| uPred_holds n x := ∀ n' x',
        x ≼ x' → n' ⪯ n → ✓{n'} x' → P n' x' → Q n' x' |}.
 Next Obligation.
@@ -351,7 +351,7 @@ Global Arguments uPred_impl {SI M}.
 Definition uPred_impl_eq :
   @uPred_impl = @uPred_impl_def := uPred_impl_aux.(seal_eq).
 
-Program Definition uPred_forall_def {SI} {M: ucmra SI} {A} (Ψ : A → uPred M) : uPred M :=
+Program Definition uPred_forall_def `{SI: indexT} {M: ucmra} {A} (Ψ : A → uPred M) : uPred M :=
   {| uPred_holds n x := ∀ a, Ψ a n x |}.
 Solve Obligations with naive_solver eauto 2 with uPred_def.
 Definition uPred_forall_aux : seal (@uPred_forall_def). Proof. by eexists. Qed.
@@ -360,7 +360,7 @@ Global Arguments uPred_forall {SI M A}.
 Definition uPred_forall_eq :
   @uPred_forall = @uPred_forall_def := uPred_forall_aux.(seal_eq).
 
-Program Definition uPred_exist_def {SI} {M: ucmra SI} {A} (Ψ : A → uPred M) : uPred M :=
+Program Definition uPred_exist_def `{SI: indexT} {M: ucmra} {A} (Ψ : A → uPred M) : uPred M :=
   {| uPred_holds n x := ∃ a, Ψ a n x |}.
 Solve Obligations with naive_solver eauto 2 with uPred_def.
 Definition uPred_exist_aux : seal (@uPred_exist_def). Proof. by eexists. Qed.
@@ -368,7 +368,7 @@ Definition uPred_exist := uPred_exist_aux.(unseal).
 Global Arguments uPred_exist {SI M A}.
 Definition uPred_exist_eq: @uPred_exist = @uPred_exist_def := uPred_exist_aux.(seal_eq).
 
-Program Definition uPred_internal_eq_def {SI} {M: ucmra SI} {A : ofe SI} (a1 a2 : A) : uPred M :=
+Program Definition uPred_internal_eq_def `{SI: indexT} {M: ucmra} {A : ofe} (a1 a2 : A) : uPred M :=
   {| uPred_holds n x := a1 ≡{n}≡ a2 |}.
 Solve Obligations with naive_solver eauto 2 using (dist_le (A:=A)).
 Definition uPred_internal_eq_aux : seal (@uPred_internal_eq_def). Proof. by eexists. Qed.
@@ -377,7 +377,7 @@ Global Arguments uPred_internal_eq {SI M A}.
 Definition uPred_internal_eq_eq:
   @uPred_internal_eq = @uPred_internal_eq_def := uPred_internal_eq_aux.(seal_eq).
 
-Program Definition uPred_sep_def {SI} {M: ucmra SI} (P Q : uPred M) : uPred M :=
+Program Definition uPred_sep_def `{SI: indexT} {M: ucmra} (P Q : uPred M) : uPred M :=
   {| uPred_holds n x := ∃ x1 x2, x ≡{n}≡ x1 ⋅ x2 ∧ P n x1 ∧ Q n x2 |}.
 Next Obligation.
   intros SI M P Q n1 n2 x y (x1&x2&Hx&?&?) [z Hy] Hn.
@@ -389,12 +389,12 @@ Definition uPred_sep := uPred_sep_aux.(unseal).
 Global Arguments uPred_sep {SI M}.
 Definition uPred_sep_eq: @uPred_sep = @uPred_sep_def := uPred_sep_aux.(seal_eq).
 
-Program Definition uPred_wand_def {SI} {M: ucmra SI} (P Q : uPred M) : uPred M :=
+Program Definition uPred_wand_def `{SI: indexT} {M: ucmra} (P Q : uPred M) : uPred M :=
   {| uPred_holds n x := ∀ n' x',
        n' ⪯ n → ✓{n'} (x ⋅ x') → P n' x' → Q n' (x ⋅ x') |}.
 Next Obligation.
   intros SI M P Q n1 n1' x1 x1' HPQ ? Hn n3 x3 ???; simpl in *.
-  eapply uPred_mono with n3 (x1 â‹… x3); last reflexivity; first eapply HPQ; first by etrans. 
+  eapply uPred_mono with n3 (x1 â‹… x3); last reflexivity; first eapply HPQ; first by etrans.
   all: eauto using cmra_validN_includedN, cmra_monoN_r, cmra_includedN_le.
 Qed.
 Definition uPred_wand_aux : seal (@uPred_wand_def). Proof. by eexists. Qed.
@@ -406,7 +406,7 @@ Definition uPred_wand_eq :
 (* Equivalently, this could be `∀ y, P n y`.  That's closer to the intuition
    of "embedding the step-indexed logic in Iris", but the two are equivalent
    because Iris is afine.  The following is easier to work with. *)
-Program Definition uPred_plainly_def {SI} {M: ucmra SI} (P : uPred M) : uPred M :=
+Program Definition uPred_plainly_def `{SI: indexT} {M: ucmra} (P : uPred M) : uPred M :=
   {| uPred_holds n x := P n ε |}.
 Solve Obligations with naive_solver eauto using uPred_mono, ucmra_unit_validN.
 Definition uPred_plainly_aux : seal (@uPred_plainly_def). Proof. by eexists. Qed.
@@ -415,7 +415,7 @@ Global Arguments uPred_plainly {SI M}.
 Definition uPred_plainly_eq :
   @uPred_plainly = @uPred_plainly_def := uPred_plainly_aux.(seal_eq).
 
-Program Definition uPred_persistently_def {SI} {M: ucmra SI} (P : uPred M) : uPred M :=
+Program Definition uPred_persistently_def `{SI: indexT} {M: ucmra} (P : uPred M) : uPred M :=
   {| uPred_holds n x := P n (core x) |}.
 Solve Obligations with naive_solver eauto using uPred_mono, @cmra_core_monoN.
 Definition uPred_persistently_aux : seal (@uPred_persistently_def). Proof. by eexists. Qed.
@@ -424,14 +424,14 @@ Global Arguments uPred_persistently {SI M}.
 Definition uPred_persistently_eq :
   @uPred_persistently = @uPred_persistently_def := uPred_persistently_aux.(seal_eq).
 
-Program Definition uPred_later_def {SI} {M: ucmra SI} (P : uPred M) : uPred M :=
+Program Definition uPred_later_def `{SI: indexT} {M: ucmra} (P : uPred M) : uPred M :=
   {| uPred_holds n x := ∀ n', n' ≺ n → P n' x |}.
 Next Obligation.
   intros SI M P n1 n2 x1 x2 H1 H2 Hle n' Hlt; simpl in *.
-  eapply uPred_mono; first eapply H1. 
-  - eauto using index_lt_le_trans. 
+  eapply uPred_mono; first eapply H1.
+  - eauto using index_lt_le_trans.
   - eauto using cmra_includedN_le.
-  - reflexivity. 
+  - reflexivity.
 Qed.
 Definition uPred_later_aux : seal (@uPred_later_def). Proof. by eexists. Qed.
 Definition uPred_later := uPred_later_aux.(unseal).
@@ -439,7 +439,7 @@ Global Arguments uPred_later {SI M}.
 Definition uPred_later_eq :
   @uPred_later = @uPred_later_def := uPred_later_aux.(seal_eq).
 
-Program Definition uPred_ownM_def {SI} {M: ucmra SI} (a : M) : uPred M :=
+Program Definition uPred_ownM_def `{SI: indexT} {M: ucmra} (a : M) : uPred M :=
   {| uPred_holds n x := a ≼{n} x |}.
 Next Obligation.
   intros SI M a n1 n2 x1 x [a' Hx1] [x2 Hx] Hn.
@@ -451,7 +451,7 @@ Global Arguments uPred_ownM {SI M}.
 Definition uPred_ownM_eq :
   @uPred_ownM = @uPred_ownM_def := uPred_ownM_aux.(seal_eq).
 
-Program Definition uPred_cmra_valid_def {SI} {M: ucmra SI} {A : cmra SI} (a : A) : uPred M :=
+Program Definition uPred_cmra_valid_def `{SI: indexT} {M: ucmra} {A : cmra} (a : A) : uPred M :=
   {| uPred_holds n x := ✓{n} a |}.
 Solve Obligations with naive_solver eauto 2 using cmra_validN_le.
 Definition uPred_cmra_valid_aux : seal (@uPred_cmra_valid_def). Proof. by eexists. Qed.
@@ -460,7 +460,7 @@ Global Arguments uPred_cmra_valid {SI M A}.
 Definition uPred_cmra_valid_eq :
   @uPred_cmra_valid = @uPred_cmra_valid_def := uPred_cmra_valid_aux.(seal_eq).
 
-Program Definition uPred_bupd_def {SI} {M: ucmra SI} (Q : uPred M) : uPred M :=
+Program Definition uPred_bupd_def `{SI: indexT} {M: ucmra} (Q : uPred M) : uPred M :=
   {| uPred_holds n x := ∀ k yf,
       k ⪯ n → ✓{k} (x ⋅ yf) → ∃ x', ✓{k} (x' ⋅ yf) ∧ Q k x' |}.
 Next Obligation.
@@ -492,7 +492,7 @@ Ltac unseal :=
   rewrite !unseal_eqs /=.
 
 Section primitive.
-Context {SI: indexT} {M : ucmra SI}.
+Context `{SI: indexT} {M : ucmra}.
 Implicit Types φ : Prop.
 Implicit Types P Q : uPred M.
 Implicit Types A : Type.
@@ -571,7 +571,7 @@ Lemma impl_ne :
   NonExpansive2 (@uPred_impl SI M).
 Proof.
   intros n P P' HP Q Q' HQ; split=> x n' ??.
-  unseal; split; intros HPQ x' n'' ????; apply HQ, HPQ, HP; 
+  unseal; split; intros HPQ x' n'' ????; apply HQ, HPQ, HP;
   match goal with |- _ ⪯ _ => first [reflexivity| by etrans]  | _ => by auto end.
 Qed.
 
@@ -588,10 +588,10 @@ Lemma wand_ne :
 Proof.
   intros n P P' HP Q Q' HQ; split=> n' x ??; unseal; split; intros HPQ x' n'' ???;
     apply HQ, HPQ, HP;
-    match goal with |- _ ⪯ _ => try reflexivity; by etrans  | _ => by eauto using cmra_validN_op_r end. 
+    match goal with |- _ ⪯ _ => try reflexivity; by etrans  | _ => by eauto using cmra_validN_op_r end.
 Qed.
 
-Lemma internal_eq_ne (A : ofe SI) :
+Lemma internal_eq_ne (A : ofe) :
   NonExpansive2 (@uPred_internal_eq SI M A).
 Proof.
   intros n x x' Hx y y' Hy; split=> n' z; unseal; split; intros; simpl in *.
@@ -637,7 +637,7 @@ Proof.
   by rewrite (dist_le _ _ _ _ Ha).
 Qed.
 
-Lemma cmra_valid_ne {A : cmra SI} :
+Lemma cmra_valid_ne {A : cmra} :
   NonExpansive (@uPred_cmra_valid SI M A).
 Proof.
   intros n a b Ha; unseal; split=> n' x ? /=.
@@ -648,9 +648,9 @@ Lemma bupd_ne : NonExpansive (@uPred_bupd SI M).
 Proof.
   intros n P Q HPQ.
   unseal; split=> n' x; split; intros HP k yf ??;
-    destruct (HP k yf) as (x'&?&?); match goal with |- ∃ _ , _ => idtac | _ => by auto end. 
+    destruct (HP k yf) as (x'&?&?); match goal with |- ∃ _ , _ => idtac | _ => by auto end.
   all: exists x'; split; auto; apply HPQ; eauto using cmra_validN_op_l.
-  all: by etrans. 
+  all: by etrans.
 Qed.
 
 (** Introduction and elimination rules *)
@@ -830,25 +830,25 @@ Lemma later_plainly_2 P : ■ ▷ P ⊢ ▷ ■ P.
 Proof. by unseal. Qed.
 
 (** Internal equality *)
-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. unseal; by split=> n x ??; simpl. Qed.
-Lemma internal_eq_rewrite {A : ofe SI} a b (Ψ : A → uPred M) :
+Lemma internal_eq_rewrite {A : ofe} a b (Ψ : A → uPred M) :
   NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b.
 Proof. intros HΨ. unseal; split=> n x ?? n' x' ??? Ha. by apply HΨ with n a. Qed.
 
-Lemma fun_ext {A} {B : A → ofe SI} (g1 g2 : discrete_fun B) :
+Lemma fun_ext {A} {B : A → ofe} (g1 g2 : discrete_fun B) :
   (∀ i, g1 i ≡ g2 i) ⊢ g1 ≡ g2.
 Proof. by unseal. Qed.
-Lemma sig_eq {A : ofe SI} (P : A → Prop) (x y : sigO P) :
+Lemma sig_eq {A : ofe} (P : A → Prop) (x y : sigO P) :
   proj1_sig x ≡ proj1_sig y ⊢ x ≡ y.
 Proof. by unseal. Qed.
 
-Lemma later_eq_1 {A : ofe SI} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y).
+Lemma later_eq_1 {A : ofe} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y).
 Proof. by unseal. Qed.
-Lemma later_eq_2 {A : ofe SI} (x y : A) : ▷ (x ≡ y) ⊢ Next x ≡ Next y.
+Lemma later_eq_2 {A : ofe} (x y : A) : ▷ (x ≡ y) ⊢ Next x ≡ Next y.
 Proof. by unseal. Qed.
 
-Lemma discrete_eq_1 {A : ofe SI} (a b : A) : Discrete a → a ≡ b ⊢ ⌜a ≡ b⌝.
+Lemma discrete_eq_1 {A : ofe} (a b : A) : Discrete a → a ≡ b ⊢ ⌜a ≡ b⌝.
 Proof.
   unseal=> ?. split=> n x ?. by apply (discrete_iff n).
 Qed.
@@ -857,7 +857,7 @@ Qed.
 between two [siProp], but we do not have the infrastructure
 to express the more general case. This temporary proof rule will
 be replaced by the proper one eventually. *)
-Lemma internal_eq_entails {A B : ofe SI} (a1 a2 : A) (b1 b2 : B) :
+Lemma internal_eq_entails {A B : ofe} (a1 a2 : A) (b1 b2 : B) :
   (∀ n, a1 ≡{n}≡ a2 → b1 ≡{n}≡ b2) → a1 ≡ a2 ⊢ b1 ≡ b2.
 Proof. unseal=>Hsi. split=>n x ?. apply Hsi. Qed.
 
@@ -909,7 +909,7 @@ Proof.
 Qed.
 Lemma ownM_unit P : P ⊢ (uPred_ownM ε).
 Proof. unseal; split=> n x ??; by  exists x; rewrite left_id. Qed.
-Lemma later_ownM `{FI: FiniteIndex SI} a : ▷ uPred_ownM a ⊢ ∃ b, uPred_ownM b ∧ ▷ (a ≡ b).
+Lemma later_ownM `{FI: !FiniteIndex SI} a : ▷ uPred_ownM a ⊢ ∃ b, uPred_ownM b ∧ ▷ (a ≡ b).
 Proof.
   unseal; split=> -n x /= ? Hax.
   destruct (finite_index n) as [->|[m ->]].
@@ -937,23 +937,23 @@ Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a.
 Proof.
   unseal; split=> n x Hv [a' ?]; ofe_subst; eauto using cmra_validN_op_l.
 Qed.
-Lemma cmra_valid_intro {A : cmra SI} P (a : A) : ✓ a → P ⊢ (✓ a).
+Lemma cmra_valid_intro {A : cmra} P (a : A) : ✓ a → P ⊢ (✓ a).
 Proof. unseal=> ?; split=> n x ? _ /=; by apply cmra_valid_validN. Qed.
-Lemma cmra_valid_elim {A : cmra SI} (a : A) : ¬ ✓{zero} a → ✓ a ⊢ False.
+Lemma cmra_valid_elim {A : cmra} (a : A) : ¬ ✓{zero} a → ✓ a ⊢ False.
 Proof. unseal=> Ha; split=> n x ??; apply Ha, cmra_validN_le with n; auto using index_zero_minimum. Qed.
-Lemma plainly_cmra_valid_1 {A : cmra SI} (a : A) : ✓ a ⊢ ■ ✓ a.
+Lemma plainly_cmra_valid_1 {A : cmra} (a : A) : ✓ a ⊢ ■ ✓ a.
 Proof. by unseal. Qed.
-Lemma cmra_valid_weaken {A : cmra SI} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
+Lemma cmra_valid_weaken {A : cmra} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
 Proof. unseal; split=> n x _; apply cmra_validN_op_l. Qed.
 
-Lemma discrete_valid {A : cmra SI} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ a⌝.
+Lemma discrete_valid {A : cmra} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ a⌝.
 Proof. unseal; split=> n x _. by rewrite /= -cmra_discrete_valid_iff. Qed.
 
 (** This is really just a special case of an entailment
 between two [siProp], but we do not have the infrastructure
 to express the more general case. This temporary proof rule will
 be replaced by the proper one eventually. *)
-Lemma valid_entails {A B : cmra SI} (a : A) (b : B) :
+Lemma valid_entails {A B : cmra} (a : A) (b : B) :
   (∀ n, ✓{n} a → ✓{n} b) → ✓ a ⊢ ✓ b.
 Proof. unseal=> Hval. split=>n x ?. apply Hval. Qed.
 
@@ -963,7 +963,7 @@ instance of [siProp] soundness in the future. *)
 Lemma pure_soundness φ : (True ⊢ ⌜ φ ⌝) → φ.
 Proof. unseal=> -[H]. by apply (H zero ε); eauto using ucmra_unit_validN. Qed.
 
-Lemma internal_eq_soundness {A : ofe SI} (x y : A) : (True ⊢ x ≡ y) → x ≡ y.
+Lemma internal_eq_soundness {A : ofe} (x y : A) : (True ⊢ x ≡ y) → x ≡ y.
 Proof.
   unseal=> -[H]. apply equiv_dist=> n.
   by apply (H n ε); eauto using ucmra_unit_validN.
@@ -973,13 +973,13 @@ Lemma later_soundness P : (True ⊢ ▷ P) → (True ⊢ P).
 Proof.
   unseal=> -[HP]; split=> n x Hx _.
   apply uPred_mono with n ε; eauto using ucmra_unit_leastN.
-  apply (HP (index_succ _ n)); eauto using ucmra_unit_validN.
+  apply (HP (index_succ n)); eauto using ucmra_unit_validN.
   constructor.
 Qed.
 
 (* satisfiabiity for uPred *)
 Definition uPred_sat (P: uPred M) :=
-    ∀ n: SI, ∃ x: M, ✓{n} x ∧ P n x.
+    ∀ n: index, ∃ x: M, ✓{n} x ∧ P n x.
 
 Lemma uPred_sat_intro: uPred_sat True.
 Proof.
@@ -1030,7 +1030,7 @@ Qed.
 
 
 (* the finite rules for BiFinite *)
-Lemma later_exist_false `{FI: FiniteIndex SI} {A} (Φ : A → uPred M) :
+Lemma later_exist_false `{FI: !FiniteIndex SI} {A} (Φ : A → uPred M) :
   (▷ ∃ a, Φ a) ⊢ ▷ False ∨ (∃ a, ▷ Φ a).
 Proof.
   unseal; split=> -n x Hv /= H; eauto.
@@ -1040,7 +1040,7 @@ Proof.
     intros; eauto using uPred_mono.
 Qed.
 
-Lemma later_sep_1 `{FI: FiniteIndex SI} P Q : ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q.
+Lemma later_sep_1 `{FI: !FiniteIndex SI} P Q : ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q.
 Proof.
   unseal; split=> n x ? //= H.
   destruct (finite_index n) as [->|[m ->]]; eauto.
@@ -1052,7 +1052,7 @@ Proof.
 Qed.
 
 (* the later or rule for BiLaterOr *)
-Lemma later_or_2 `{FBE: FiniteBoundedExistential SI} (P Q: uPred M):
+Lemma later_or_2 `{FBE: !FiniteBoundedExistential SI} (P Q: uPred M):
   ▷ (P ∨ Q) ⊢ ▷ P ∨ ▷ Q.
 Proof.
   unseal; split=> -n x Hv /= H; eauto.
@@ -1070,7 +1070,7 @@ Definition timeless (P: uPred M) := ▷ P ⊢ ▷ False ∨ P.
 Lemma timeless_alt P: (timeless P) ↔ ((▷ False → P) ⊢ P).
 Proof.
   unfold timeless; unseal; split; intros [H]; split=> n x Hv //= HP; simpl in *.
-  - induction n  as [n IH] using (well_founded_ind (index_lt_wf SI)).
+  - induction n  as [n IH] using (well_founded_ind (index_lt_wf)).
     destruct (index_lt_dec_minimum n) as [H'|[m ?]]; eauto.
     edestruct H; eauto.
     intros; eapply IH; eauto using cmra_validN_le, index_le_lt_trans.
diff --git a/theories/bi/lib/fixpoint.v b/theories/bi/lib/fixpoint.v
index ffcdb2546a6f7284e37515b51d4a796239496a1d..16ee45109fb80237a0a97e7cd75323f6c8b916e7 100644
--- a/theories/bi/lib/fixpoint.v
+++ b/theories/bi/lib/fixpoint.v
@@ -5,34 +5,34 @@ Import bi.
 
 (** Least and greatest fixpoint of a monotone function, defined entirely inside
     the logic.  *)
-Class BiMonoPred {SI} {PROP : bi SI} {A : ofe SI} (F : (A → PROP) → (A → PROP)) := {
+Class BiMonoPred `{SI: indexT} {PROP : bi} {A : ofe} (F : (A → PROP) → (A → PROP)) := {
   bi_mono_pred Φ Ψ : ⊢ <pers> (∀ x, Φ x -∗ Ψ x) → ∀ x, F Φ x -∗ F Ψ x;
   bi_mono_pred_ne Φ : NonExpansive Φ → NonExpansive (F Φ)
 }.
 Global Arguments bi_mono_pred {_ _ _ _ _} _ _.
 Local Existing Instance bi_mono_pred_ne.
 
-Definition bi_least_fixpoint {SI} {PROP : bi SI} {A : ofe SI}
+Definition bi_least_fixpoint `{SI: indexT} {PROP : bi} {A : ofe}
     (F : (A → PROP) → (A → PROP)) (x : A) : PROP :=
   tc_opaque (∀ Φ : A -n> PROP, <pers> (∀ x, F Φ x -∗ Φ x) → Φ x)%I.
 Global Arguments bi_least_fixpoint : simpl never.
 
-Definition bi_greatest_fixpoint {SI} {PROP : bi SI} {A : ofe SI}
+Definition bi_greatest_fixpoint `{SI: indexT} {PROP : bi} {A : ofe}
     (F : (A → PROP) → (A → PROP)) (x : A) : PROP :=
   tc_opaque (∃ Φ : A -n> PROP, <pers> (∀ x, Φ x -∗ F Φ x) ∧ Φ x)%I.
 Global Arguments bi_greatest_fixpoint : simpl never.
 
-Global Instance least_fixpoint_ne {SI} {PROP : bi SI} {A : ofe SI} n :
+Global Instance least_fixpoint_ne `{SI: indexT} {PROP : bi} {A : ofe} n :
   Proper (pointwise_relation (A → PROP) (pointwise_relation A (dist n)) ==>
           dist n ==> dist n) bi_least_fixpoint.
 Proof. solve_proper. Qed.
-Global Instance least_fixpoint_proper {SI} {PROP : bi SI} {A : ofe SI} :
+Global Instance least_fixpoint_proper `{SI: indexT} {PROP : bi} {A : ofe} :
   Proper (pointwise_relation (A → PROP) (pointwise_relation A (≡)) ==>
           (≡) ==> (≡)) bi_least_fixpoint.
 Proof. solve_proper. Qed.
 
 Section least.
-  Context {SI} {PROP : bi SI} {A : ofe SI} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.
+  Context `{SI: indexT} {PROP : bi} {A : ofe} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.
 
   Lemma least_fixpoint_unfold_2 x : F (bi_least_fixpoint F) x ⊢ bi_least_fixpoint F x.
   Proof using Type*.
@@ -74,7 +74,7 @@ Section least.
   Qed.
 End least.
 
-Lemma greatest_fixpoint_ne_outer {SI} {PROP : bi SI} {A : ofe SI}
+Lemma greatest_fixpoint_ne_outer `{SI: indexT} {PROP : bi} {A : ofe}
     (F1 : (A → PROP) → (A → PROP)) (F2 : (A → PROP) → (A → PROP)):
   (∀ Φ x n, F1 Φ x ≡{n}≡ F2 Φ x) → ∀ x1 x2 n,
   x1 ≡{n}≡ x2 → bi_greatest_fixpoint F1 x1 ≡{n}≡ bi_greatest_fixpoint F2 x2.
@@ -83,17 +83,17 @@ Proof.
   do 3 f_equiv; last solve_proper. repeat f_equiv. apply HF.
 Qed.
 
-Global Instance greatest_fixpoint_ne {SI} {PROP : bi SI} {A : ofe SI} n :
+Global Instance greatest_fixpoint_ne `{SI: indexT} {PROP : bi} {A : ofe} n :
   Proper (pointwise_relation (A → PROP) (pointwise_relation A (dist n)) ==>
           dist n ==> dist n) bi_greatest_fixpoint.
 Proof. solve_proper. Qed.
-Global Instance greatest_fixpoint_proper {SI} {PROP : bi SI} {A : ofe SI} :
+Global Instance greatest_fixpoint_proper `{SI: indexT} {PROP : bi} {A : ofe} :
   Proper (pointwise_relation (A → PROP) (pointwise_relation A (≡)) ==>
           (≡) ==> (≡)) bi_greatest_fixpoint.
 Proof. solve_proper. Qed.
 
 Section greatest.
-  Context {SI} {PROP : bi SI} {A : ofe SI} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.
+  Context `{SI: indexT} {PROP : bi} {A : ofe} (F : (A → PROP) → (A → PROP)) `{!BiMonoPred F}.
 
   Lemma greatest_fixpoint_unfold_1 x :
     bi_greatest_fixpoint F x ⊢ F (bi_greatest_fixpoint F) x.
diff --git a/theories/bi/lib/fractional.v b/theories/bi/lib/fractional.v
index 8a18fdc682ef956dcbc9649600dc07b20d4dbd34..94c4f08e5cd6ea1db258d4011e71aed44279c998 100644
--- a/theories/bi/lib/fractional.v
+++ b/theories/bi/lib/fractional.v
@@ -2,11 +2,11 @@ From iris.bi Require Export bi.
 From iris.proofmode Require Import classes class_instances.
 From iris.prelude Require Import options.
 
-Class Fractional {SI} {PROP : bi SI} (Φ : Qp → PROP) :=
+Class Fractional `{SI: indexT} {PROP : bi} (Φ : Qp → PROP) :=
   fractional p q : Φ (p + q)%Qp ⊣⊢ Φ p ∗ Φ q.
 Arguments Fractional {_ _} _%I : simpl never.
 
-Class AsFractional {SI} {PROP : bi SI} (P : PROP) (Φ : Qp → PROP) (q : Qp) := {
+Class AsFractional `{SI: indexT} {PROP : bi} (P : PROP) (Φ : Qp → PROP) (q : Qp) := {
   as_fractional : P ⊣⊢ Φ q;
   as_fractional_fractional :> Fractional Φ
 }.
@@ -20,7 +20,7 @@ allow [q] to be an evar. *)
 Global Hint Mode AsFractional - - - + - : typeclass_instances.
 
 Section fractional.
-  Context {SI} {PROP : bi SI}.
+  Context `{SI: indexT} {PROP : bi}.
   Implicit Types P Q : PROP.
   Implicit Types Φ : Qp → PROP.
   Implicit Types q : Qp.
diff --git a/theories/proofmode/class_instances.v b/theories/proofmode/class_instances.v
index 22d45400ad44e167ba85a2f344bd07a017b8051e..4795bb9261f4572703836a6846817165b0451a12 100644
--- a/theories/proofmode/class_instances.v
+++ b/theories/proofmode/class_instances.v
@@ -12,7 +12,7 @@ algorithm. We use [shelve] to avoid the creation of unshelved goals for evars
 by [refine], which otherwise causes TC search to fail. Such unshelved goals are
 created for example when solving [FromAssumption p ?P ?Q] where both [?P] and
 [?Q] are evars. See [test_iApply_evar] in [tests/proofmode] for an example. *)
-Lemma from_assumption_exact {SI} {PROP : bi SI} p (P : PROP) : FromAssumption p P P.
+Lemma from_assumption_exact `{SI: indexT} {PROP : bi} p (P : PROP) : FromAssumption p P P.
 Proof. by rewrite /FromAssumption /= intuitionistically_if_elim. Qed.
 Global Hint Extern 0 (FromAssumption _ _ _) =>
   notypeclasses refine (from_assumption_exact _ _); shelve : typeclass_instances.
@@ -21,13 +21,13 @@ Global Hint Extern 0 (FromAssumption _ _ _) =>
 (** Similarly, the lemma [from_exist_exist] is defined using a [Hint Extern] to
 enable the better unification algorithm.
 See https://gitlab.mpi-sws.org/iris/iris/issues/288 *)
-Lemma from_exist_exist {SI} {PROP : bi SI} {A} (Φ : A → PROP) : FromExist (∃ a, Φ a) Φ.
+Lemma from_exist_exist `{SI: indexT} {PROP : bi} {A} (Φ : A → PROP) : FromExist (∃ a, Φ a) Φ.
 Proof. by rewrite /FromExist. Qed.
 Global Hint Extern 0 (FromExist _ _) =>
   notypeclasses refine (from_exist_exist _) : typeclass_instances.
 
 Section class_instances.
-Context {SI} {PROP : bi SI}.
+Context `{SI: indexT} {PROP : bi}.
 Implicit Types P Q R : PROP.
 Implicit Types mP : option PROP.
 
diff --git a/theories/proofmode/class_instances_embedding.v b/theories/proofmode/class_instances_embedding.v
index 644b3d106fb0d9a6ab5e44ae9403fabda0c93a7d..c2dcfe830b425036e06045c3ddaddfceb24a23b0 100644
--- a/theories/proofmode/class_instances_embedding.v
+++ b/theories/proofmode/class_instances_embedding.v
@@ -7,13 +7,13 @@ Import bi.
 instance is not used when there is no embedding between [PROP] and [PROP']. The
 first [`{BiEmbed PROP PROP'}] is not considered as a premise by Coq TC search
 mechanism because the rest of the hypothesis is dependent on it. *)
-Global Instance as_emp_valid_embed {SI} {PROP PROP': bi SI} `{!BiEmbed PROP PROP'} (φ : Prop) (P : PROP) :
+Global Instance as_emp_valid_embed `{SI: indexT} {PROP PROP': bi} `{!BiEmbed PROP PROP'} (φ : Prop) (P : PROP) :
   BiEmbed PROP PROP' →
   AsEmpValid0 φ P → AsEmpValid φ ⎡P⎤.
 Proof. rewrite /AsEmpValid0 /AsEmpValid=> _ ->. rewrite embed_emp_valid //. Qed.
 
 Section class_instances_embedding.
-Context {SI} {PROP PROP': bi SI} `{!BiEmbed PROP PROP'}.
+Context `{SI: indexT} {PROP PROP': bi} `{!BiEmbed PROP PROP'}.
 Implicit Types P Q R : PROP.
 
 Global Instance into_pure_embed P φ :
@@ -152,7 +152,7 @@ Proof. rewrite /FromModal /= =><-. by rewrite embed_plainly. Qed.
 
 Global Instance into_internal_eq_embed
     `{!BiInternalEq PROP, !BiInternalEq PROP', !BiEmbedInternalEq PROP PROP'}
-    {A : ofe SI} (x y : A) (P : PROP) :
+    {A : ofe} (x y : A) (P : PROP) :
   IntoInternalEq P x y → IntoInternalEq (⎡P⎤ : PROP')%I x y.
 Proof. rewrite /IntoInternalEq=> ->. by rewrite embed_internal_eq. Qed.
 
diff --git a/theories/proofmode/class_instances_internal_eq.v b/theories/proofmode/class_instances_internal_eq.v
index d226c82175f2fdd9dae13b134e438d97355a63d0..3a3b5d4621e12b27460593089cb64fc4814f10c7 100644
--- a/theories/proofmode/class_instances_internal_eq.v
+++ b/theories/proofmode/class_instances_internal_eq.v
@@ -5,23 +5,23 @@ From iris.prelude Require Import options.
 Import bi.
 
 Section class_instances_internal_eq.
-Context {SI} {PROP: bi SI} `{!BiInternalEq PROP}.
+Context `{SI: indexT} {PROP: bi} `{!BiInternalEq PROP}.
 Implicit Types P Q R : PROP.
 
-Global Instance from_pure_internal_eq {A : ofe SI} (a b : A) :
+Global Instance from_pure_internal_eq {A : ofe} (a b : A) :
   @FromPure SI PROP false (a ≡ b) (a ≡ b).
 Proof. by rewrite /FromPure pure_internal_eq. Qed.
 
-Global Instance into_pure_eq {A : ofe SI} (a b : A) :
+Global Instance into_pure_eq {A : ofe} (a b : A) :
   Discrete a → @IntoPure SI PROP (a ≡ b) (a ≡ b).
 Proof. intros. by rewrite /IntoPure discrete_eq. Qed.
 
-Global Instance from_modal_Next {A : ofe SI} (x y : A) :
+Global Instance from_modal_Next {A : ofe} (x y : A) :
   FromModal (PROP1:=PROP) (PROP2:=PROP) (modality_laterN 1)
     (▷^1 (x ≡ y) : PROP)%I (Next x ≡ Next y) (x ≡ y).
 Proof. by rewrite /FromModal /= later_equivI. Qed.
 
-Global Instance into_laterN_Next {A : ofe SI} only_head n n' (x y : A) :
+Global Instance into_laterN_Next {A : ofe} only_head n n' (x y : A) :
   NatCancel n 1 n' 0 →
   IntoLaterN (PROP:=PROP) only_head n (Next x ≡ Next y) (x ≡ y) | 2.
 Proof.
@@ -29,22 +29,22 @@ Proof.
   move=> <-. rewrite later_equivI. by rewrite Nat.add_comm /= -laterN_intro.
 Qed.
 
-Global Instance into_internal_eq_internal_eq {A : ofe SI} (x y : A) :
+Global Instance into_internal_eq_internal_eq {A : ofe} (x y : A) :
   @IntoInternalEq SI PROP _ A (x ≡ y) x y.
 Proof. by rewrite /IntoInternalEq. Qed.
-Global Instance into_internal_eq_affinely {A : ofe SI} (x y : A) P :
+Global Instance into_internal_eq_affinely {A : ofe} (x y : A) P :
   IntoInternalEq P x y → IntoInternalEq (<affine> P) x y.
 Proof. rewrite /IntoInternalEq=> ->. by rewrite affinely_elim. Qed.
-Global Instance into_internal_eq_intuitionistically {A : ofe SI} (x y : A) P :
+Global Instance into_internal_eq_intuitionistically {A : ofe} (x y : A) P :
   IntoInternalEq P x y → IntoInternalEq (□ P) x y.
 Proof. rewrite /IntoInternalEq=> ->. by rewrite intuitionistically_elim. Qed.
-Global Instance into_internal_eq_absorbingly {A : ofe SI} (x y : A) P :
+Global Instance into_internal_eq_absorbingly {A : ofe} (x y : A) P :
   IntoInternalEq P x y → IntoInternalEq (<absorb> P) x y.
 Proof. rewrite /IntoInternalEq=> ->. by rewrite absorbingly_internal_eq. Qed.
-Global Instance into_internal_eq_plainly `{!BiPlainly PROP} {A : ofe SI} (x y : A) P :
+Global Instance into_internal_eq_plainly `{!BiPlainly PROP} {A : ofe} (x y : A) P :
   IntoInternalEq P x y → IntoInternalEq (■ P) x y.
 Proof. rewrite /IntoInternalEq=> ->. by rewrite plainly_elim. Qed.
-Global Instance into_internal_eq_persistently {A : ofe SI} (x y : A) P :
+Global Instance into_internal_eq_persistently {A : ofe} (x y : A) P :
   IntoInternalEq P x y → IntoInternalEq (<pers> P) x y.
 Proof. rewrite /IntoInternalEq=> ->. by rewrite persistently_elim. Qed.
 End class_instances_internal_eq.
\ No newline at end of file
diff --git a/theories/proofmode/class_instances_later.v b/theories/proofmode/class_instances_later.v
index f9915fcd1d59ee26a3dd52306d75883facf608d6..f77465ac33476534cbb7cb43593102105f147c0e 100644
--- a/theories/proofmode/class_instances_later.v
+++ b/theories/proofmode/class_instances_later.v
@@ -5,7 +5,7 @@ From iris.prelude Require Import options.
 Import bi.
 
 Section class_instances_later.
-Context {SI} {PROP : bi SI}.
+Context `{SI: indexT} {PROP : bi}.
 Implicit Types P Q R : PROP.
 
 (** FromAssumption *)
@@ -338,7 +338,7 @@ Global Instance into_later_intuitionistically n P Q :
   IntoLaterN false n P Q → IntoLaterN false n (□ P) (□ Q).
 Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_intuitionistically_2. Qed.
 (* FIXME: currently depends on BiAffine because of laterN_absorbingly *)
-Global Instance into_later_absorbingly `{BiAffine SI PROP} n P Q :
+Global Instance into_later_absorbingly `{!BiAffine PROP} n P Q :
   IntoLaterN false n P Q → IntoLaterN false n (<absorb> P) (<absorb> Q).
 Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_absorbingly. Qed.
 Global Instance into_later_persistently n P Q :
diff --git a/theories/proofmode/class_instances_plainly.v b/theories/proofmode/class_instances_plainly.v
index 72d2410bc67ae9794d8bed69895ca8fa698d6a1a..30064237287031bba44511f8f9526a5734c04628 100644
--- a/theories/proofmode/class_instances_plainly.v
+++ b/theories/proofmode/class_instances_plainly.v
@@ -4,7 +4,7 @@ From iris.prelude Require Import options.
 Import bi.
 
 Section class_instances_plainly.
-Context {SI} {PROP: bi SI} `{!BiPlainly PROP}.
+Context `{SI: indexT} {PROP: bi} `{!BiPlainly PROP}.
 Implicit Types P Q R : PROP.
 
 Global Instance from_assumption_plainly_l_true P Q :
diff --git a/theories/proofmode/class_instances_updates.v b/theories/proofmode/class_instances_updates.v
index 57cf1540f2a40f60c144787c4e349285fbe69cdf..c85ce47f9928d0144d839ce697ac7fd2300261a7 100644
--- a/theories/proofmode/class_instances_updates.v
+++ b/theories/proofmode/class_instances_updates.v
@@ -6,7 +6,7 @@ From iris.prelude Require Import options.
 Import bi.
 
 Section class_instances_updates.
-Context {SI} {PROP : bi SI}.
+Context `{SI: indexT} {PROP : bi}.
 Implicit Types P Q R : PROP.
 
 Global Instance from_assumption_bupd `{!BiBUpd PROP} p P Q :
diff --git a/theories/proofmode/classes.v b/theories/proofmode/classes.v
index edf0e79cecd876382b406df895a0faab8d99c8c9..d7199bc5ea9963cdcbf37bde31a8919418d29535 100644
--- a/theories/proofmode/classes.v
+++ b/theories/proofmode/classes.v
@@ -5,25 +5,25 @@ From iris.proofmode Require Export ident_name modalities.
 From iris.prelude Require Import options.
 Import bi.
 
-Class FromAssumption {SI} {PROP : bi SI} (p : bool) (P Q : PROP) :=
+Class FromAssumption `{SI: indexT} {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 Hint Mode FromAssumption - + + - - : typeclass_instances.
 
-Class KnownLFromAssumption {SI} {PROP : bi SI} (p : bool) (P Q : PROP) :=
+Class KnownLFromAssumption `{SI: indexT} {PROP : bi} (p : bool) (P Q : PROP) :=
   knownl_from_assumption :> FromAssumption p P Q.
 Global Arguments KnownLFromAssumption {_ _} _ _%I _%I : simpl never.
 Global Arguments knownl_from_assumption {_ _} _ _%I _%I {_}.
 Global Hint Mode KnownLFromAssumption - + + ! - : typeclass_instances.
 
-Class KnownRFromAssumption {SI} {PROP : bi SI} (p : bool) (P Q : PROP) :=
+Class KnownRFromAssumption `{SI: indexT} {PROP : bi} (p : bool) (P Q : PROP) :=
   knownr_from_assumption :> FromAssumption p P Q.
 Global Arguments KnownRFromAssumption {_ _} _ _%I _%I : simpl never.
 Global Arguments knownr_from_assumption {_ _} _ _%I _%I {_}.
 Global Hint Mode KnownRFromAssumption - + + - ! : typeclass_instances.
 
-Class IntoPure {SI} {PROP : bi SI} (P : PROP) (φ : Prop) :=
+Class IntoPure `{SI: indexT} {PROP : bi} (P : PROP) (φ : Prop) :=
   into_pure : P ⊢ ⌜φ⌝.
 Global Arguments IntoPure {_ _} _%I _%type_scope : simpl never.
 Global Arguments into_pure {_ _} _%I _%type_scope {_}.
@@ -49,9 +49,9 @@ once, and use [IntoPureT] in any instance like [into_exist_and_pure].
 
 TODO: Report this as a Coq bug, or wait for https://github.com/coq/coq/pull/991
 to be finished and merged someday. *)
-Class IntoPureT {SI} {PROP : bi SI} (P : PROP) (φ : Type) :=
+Class IntoPureT `{SI: indexT} {PROP : bi} (P : PROP) (φ : Type) :=
   into_pureT : ∃ ψ : Prop, φ = ψ ∧ IntoPure P ψ.
-Lemma into_pureT_hint {SI} {PROP : bi SI} (P : PROP) (φ : Prop) : IntoPure P φ → IntoPureT P φ.
+Lemma into_pureT_hint `{SI: indexT} {PROP : bi} (P : PROP) (φ : Prop) : IntoPure P φ → IntoPureT P φ.
 Proof. by exists φ. Qed.
 Global Hint Extern 0 (IntoPureT _ _) =>
   notypeclasses refine (into_pureT_hint _ _ _) : typeclass_instances.
@@ -65,27 +65,27 @@ the spatial context should be empty or not.
 
 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 {SI} {PROP : bi SI} (a : bool) (P : PROP) (φ : Prop) :=
+Class FromPure `{SI: indexT} {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 Hint Mode FromPure - + - ! - : typeclass_instances.
 
-Class FromPureT {SI} {PROP : bi SI} (a : bool) (P : PROP) (φ : Type) :=
+Class FromPureT `{SI: indexT} {PROP : bi} (a : bool) (P : PROP) (φ : Type) :=
   from_pureT : ∃ ψ : Prop, φ = ψ ∧ FromPure a P ψ.
-Lemma from_pureT_hint {SI} {PROP : bi SI} (a : bool) (P : PROP) (φ : Prop) :
+Lemma from_pureT_hint `{SI: indexT} {PROP : bi} (a : bool) (P : PROP) (φ : Prop) :
   FromPure a P φ → FromPureT a P φ.
 Proof. by exists φ. Qed.
 Global Hint Extern 0 (FromPureT _ _ _) =>
   notypeclasses refine (from_pureT_hint _ _ _ _) : typeclass_instances.
 
-Class IntoInternalEq {SI} {PROP : bi SI} `{!BiInternalEq PROP} {A : ofe SI} (P : PROP) (x y : A) :=
+Class IntoInternalEq `{SI: indexT} {PROP : bi} `{!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 Hint Mode IntoInternalEq - + - - ! - - : typeclass_instances.
 
-Class IntoPersistent {SI} {PROP : bi SI} (p : bool) (P Q : PROP) :=
+Class IntoPersistent `{SI: indexT} {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 {_}.
@@ -107,7 +107,7 @@ can define an instance [FromModal modality_id (N P) P]. Defining such an
 instance only imposes the proof obligation [P ⊢ N P]. Examples of such
 modalities [N] are [bupd], [fupd], [except_0], [monPred_subjectively] and
 [bi_absorbingly]. *)
-Class FromModal {SI} {PROP1 PROP2 : bi SI} {A}
+Class FromModal `{SI: indexT} {PROP1 PROP2 : bi} {A}
     (M : modality PROP1 PROP2) (sel : A) (P : PROP2) (Q : PROP1) :=
   from_modal : M Q ⊢ P.
 Global Arguments FromModal {_ _ _ _} _ _%I _%I _%I : simpl never.
@@ -118,7 +118,7 @@ Global Hint Mode FromModal - - + - - - ! - : typeclass_instances.
 proposition [Q].
 
 The input is [Q] and the output is [P]. *)
-Class FromAffinely {SI} {PROP : bi SI} (P Q : PROP) :=
+Class FromAffinely `{SI: indexT} {PROP : bi} (P Q : PROP) :=
   from_affinely : <affine> Q ⊢ P.
 Global Arguments FromAffinely {_ _} _%I _%I : simpl never.
 Global Arguments from_affinely {_ _} _%I _%I {_}.
@@ -128,7 +128,7 @@ Global Hint Mode FromAffinely - + - ! : typeclass_instances.
 the proposition [Q].
 
 The input is [Q] and the output is [P]. *)
-Class IntoAbsorbingly {SI} {PROP : bi SI} (P Q : PROP) :=
+Class IntoAbsorbingly `{SI: indexT} {PROP : bi} (P Q : PROP) :=
   into_absorbingly : P ⊢ <absorb> Q.
 Global Arguments IntoAbsorbingly {_ _} _%I _%I.
 Global Arguments into_absorbingly {_ _} _%I _%I {_}.
@@ -143,87 +143,87 @@ Global Hint Mode IntoAbsorbingly - + - ! : typeclass_instances.
   hypothesis).
 - Instantiate the premise of the wand or implication. *)
 
-Class IntoWand {SI} {PROP : bi SI} (p q : bool) (R P Q : PROP) :=
+Class IntoWand `{SI: indexT} {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 Hint Mode IntoWand - + + + ! - - : typeclass_instances.
 
-Class IntoWand' {SI} {PROP : bi SI} (p q : bool) (R P Q : PROP) :=
+Class IntoWand' `{SI: indexT} {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 Hint Mode IntoWand' - + + + ! ! - : typeclass_instances.
 Global Hint Mode IntoWand' - + + + ! - ! : typeclass_instances.
 
-Class FromWand {SI} {PROP : bi SI} (P Q1 Q2 : PROP) := from_wand : (Q1 -∗ Q2) ⊢ P.
+Class FromWand `{SI: indexT} {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 Hint Mode FromWand - + ! - - : typeclass_instances.
 
-Class FromImpl {SI} {PROP : bi SI} (P Q1 Q2 : PROP) := from_impl : (Q1 → Q2) ⊢ P.
+Class FromImpl `{SI: indexT} {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 Hint Mode FromImpl - + ! - - : typeclass_instances.
 
-Class FromSep {SI} {PROP : bi SI} (P Q1 Q2 : PROP) := from_sep : Q1 ∗ Q2 ⊢ P.
+Class FromSep `{SI: indexT} {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 Hint Mode FromSep - + ! - - : typeclass_instances.
 Global Hint Mode FromSep - + - ! ! : typeclass_instances. (* For iCombine *)
 
-Class FromAnd {SI} {PROP : bi SI} (P Q1 Q2 : PROP) := from_and : Q1 ∧ Q2 ⊢ P.
+Class FromAnd `{SI: indexT} {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 Hint Mode FromAnd - + ! - - : typeclass_instances.
 Global Hint Mode FromAnd - + - ! ! : typeclass_instances. (* For iCombine *)
 
-Class IntoAnd {SI} {PROP : bi SI} (p : bool) (P Q1 Q2 : PROP) :=
+Class IntoAnd `{SI: indexT} {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 Hint Mode IntoAnd - + + ! - - : typeclass_instances.
 
-Class IntoSep {SI} {PROP : bi SI} (P Q1 Q2 : PROP) :=
+Class IntoSep `{SI: indexT} {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 Hint Mode IntoSep - + ! - - : typeclass_instances.
 
-Class FromOr {SI} {PROP : bi SI} (P Q1 Q2 : PROP) := from_or : Q1 ∨ Q2 ⊢ P.
+Class FromOr `{SI: indexT} {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 Hint Mode FromOr - + ! - - : typeclass_instances.
 
-Class IntoOr {SI} {PROP : bi SI} (P Q1 Q2 : PROP) := into_or : P ⊢ Q1 ∨ Q2.
+Class IntoOr `{SI: indexT} {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 Hint Mode IntoOr - + ! - - : typeclass_instances.
 
-Class FromExist {SI} {PROP : bi SI} {A} (P : PROP) (Φ : A → PROP) :=
+Class FromExist `{SI: indexT} {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 Hint Mode FromExist - + - ! - : typeclass_instances.
 
-Class IntoExist {SI} {PROP : bi SI} {A} (P : PROP) (Φ : A → PROP) (name: ident_name) :=
+Class IntoExist `{SI: indexT} {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 Hint Mode IntoExist - + - ! - - : typeclass_instances.
 
-Class IntoForall {SI} {PROP : bi SI} {A} (P : PROP) (Φ : A → PROP) :=
+Class IntoForall `{SI: indexT} {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 Hint Mode IntoForall - + - ! - : typeclass_instances.
 
-Class FromForall {SI} {PROP : bi SI} {A} (P : PROP) (Φ : A → PROP) (name : ident_name) :=
+Class FromForall `{SI: indexT} {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 Hint Mode FromForall - + - ! - - : typeclass_instances.
 
-Class IsExcept0 {SI} {PROP : bi SI} (Q : PROP) := is_except_0 : ◇ Q ⊢ Q.
+Class IsExcept0 `{SI: indexT} {PROP : bi} (Q : PROP) := is_except_0 : ◇ Q ⊢ Q.
 Global Arguments IsExcept0 {_ _} _%I : simpl never.
 Global Arguments is_except_0 {_ _} _%I {_}.
 Global Hint Mode IsExcept0 - + ! : typeclass_instances.
@@ -247,7 +247,7 @@ transformed from [|={E1,E3}=> Q] into [|={E2,E3}=> Q], and the resulting
 hypothesis is moved into the spatial context (regardless of where it was
 originally). A corresponding [ElimModal] instance for the Iris 1/2-style update
 modality, would have a side-condition [φ] on the masks. *)
-Class ElimModal {SI} {PROP : bi SI} (φ : Prop) (p p' : bool) (P P' : PROP) (Q Q' : PROP) :=
+Class ElimModal `{SI: indexT} {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 {_}.
@@ -255,13 +255,13 @@ 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 {SI} {PROP : bi SI} (P P' : PROP) (Q : PROP) :=
+Class AddModal `{SI: indexT} {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 Hint Mode AddModal - + - ! ! : typeclass_instances.
 
-Lemma add_modal_id {SI} {PROP : bi SI} (P Q : PROP) : AddModal P P Q.
+Lemma add_modal_id `{SI: indexT} {PROP : bi} (P Q : PROP) : AddModal P P Q.
 Proof. by rewrite /AddModal wand_elim_r. Qed.
 
 (** We use the classes [IsCons] and [IsApp] to make sure that instances such as
@@ -277,7 +277,7 @@ Proof. done. Qed.
 Global Instance is_app_app {A} (l1 l2 : list A) : IsApp (l1 ++ l2) l1 l2.
 Proof. done. Qed.
 
-Class Frame {SI} {PROP : bi SI} (p : bool) (R P Q : PROP) := frame : □?p R ∗ Q ⊢ P.
+Class Frame `{SI: indexT} {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 Hint Mode Frame - + + ! ! - : typeclass_instances.
@@ -285,20 +285,20 @@ Global Hint Mode Frame - + + ! ! - : typeclass_instances.
 (* The boolean [progress] indicates whether actual framing has been performed.
 If it is [false], then the default instance [maybe_frame_default] below has been
 used. *)
-Class MaybeFrame {SI} {PROP : bi SI} (p : bool) (R P Q : PROP) (progress : bool) :=
+Class MaybeFrame `{SI: indexT} {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 Hint Mode MaybeFrame - + + ! - - - : typeclass_instances.
 
-Global Instance maybe_frame_frame {SI} {PROP : bi SI} p (R P Q : PROP) :
+Global Instance maybe_frame_frame `{SI: indexT} {PROP : bi} p (R P Q : PROP) :
   Frame p R P Q → MaybeFrame p R P Q true.
 Proof. done. Qed.
 
-Global Instance maybe_frame_default_persistent {SI} {PROP : bi SI} (R P : PROP) :
+Global Instance maybe_frame_default_persistent `{SI: indexT} {PROP : bi} (R P : PROP) :
   MaybeFrame true R P P false | 100.
 Proof. intros. rewrite /MaybeFrame /=. by rewrite sep_elim_r. Qed.
-Global Instance maybe_frame_default {SI} {PROP : bi SI} (R P : PROP) :
+Global Instance maybe_frame_default `{SI: indexT} {PROP : bi} (R P : PROP) :
   TCOr (Affine R) (Absorbing P) → MaybeFrame false R P P false | 100.
 Proof. intros. rewrite /MaybeFrame /=. apply: sep_elim_r. Qed.
 
@@ -312,105 +312,105 @@ Proof. intros. rewrite /MaybeFrame /=. apply: sep_elim_r. Qed.
    logical constructs such as emp or True. Therefore, we use a Hint
    Mode to disable all the instances that would have this behavior. *)
 
-Class MakeEmbed {SI} {PROP PROP' : bi SI} `{BiEmbed SI PROP PROP'} (P : PROP) (Q : PROP') :=
+Class MakeEmbed `{SI: indexT} {PROP PROP' : bi} `{!BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
   make_embed : ⎡P⎤ ⊣⊢ Q.
 Global Arguments MakeEmbed {_ _ _ _} _%I _%I.
 Global Hint Mode MakeEmbed - + + + - - : typeclass_instances.
-Class KnownMakeEmbed {SI} {PROP PROP' : bi SI} `{BiEmbed SI PROP PROP'} (P : PROP) (Q : PROP') :=
+Class KnownMakeEmbed `{SI: indexT} {PROP PROP' : bi} `{!BiEmbed PROP PROP'} (P : PROP) (Q : PROP') :=
   known_make_embed :> MakeEmbed P Q.
 Global Arguments KnownMakeEmbed {_ _ _ _} _%I _%I.
 Global Hint Mode KnownMakeEmbed - + + + ! - : typeclass_instances.
 
-Class MakeSep {SI} {PROP : bi SI} (P Q PQ : PROP) := make_sep : P ∗ Q ⊣⊢ PQ .
+Class MakeSep `{SI: indexT} {PROP : bi} (P Q PQ : PROP) := make_sep : P ∗ Q ⊣⊢ PQ .
 Global Arguments MakeSep {_ _} _%I _%I _%I.
 Global Hint Mode MakeSep - + - - - : typeclass_instances.
-Class KnownLMakeSep {SI} {PROP : bi SI} (P Q PQ : PROP) :=
+Class KnownLMakeSep `{SI: indexT} {PROP : bi} (P Q PQ : PROP) :=
   knownl_make_sep :> MakeSep P Q PQ.
 Global Arguments KnownLMakeSep {_ _} _%I _%I _%I.
 Global Hint Mode KnownLMakeSep - + ! - - : typeclass_instances.
-Class KnownRMakeSep {SI} {PROP : bi SI} (P Q PQ : PROP) :=
+Class KnownRMakeSep `{SI: indexT} {PROP : bi} (P Q PQ : PROP) :=
   knownr_make_sep :> MakeSep P Q PQ.
 Global Arguments KnownRMakeSep {_ _} _%I _%I _%I.
 Global Hint Mode KnownRMakeSep - + - ! - : typeclass_instances.
 
-Class MakeAnd {SI} {PROP : bi SI} (P Q PQ : PROP) :=  make_and_l : P ∧ Q ⊣⊢ PQ.
+Class MakeAnd `{SI: indexT} {PROP : bi} (P Q PQ : PROP) :=  make_and_l : P ∧ Q ⊣⊢ PQ.
 Global Arguments MakeAnd {_ _} _%I _%I _%I.
 Global Hint Mode MakeAnd - + - - - : typeclass_instances.
-Class KnownLMakeAnd {SI} {PROP : bi SI} (P Q PQ : PROP) :=
+Class KnownLMakeAnd `{SI: indexT} {PROP : bi} (P Q PQ : PROP) :=
   knownl_make_and :> MakeAnd P Q PQ.
 Global Arguments KnownLMakeAnd {_ _} _%I _%I _%I.
 Global Hint Mode KnownLMakeAnd - + ! - - : typeclass_instances.
-Class KnownRMakeAnd {SI} {PROP : bi SI} (P Q PQ : PROP) :=
+Class KnownRMakeAnd `{SI: indexT} {PROP : bi} (P Q PQ : PROP) :=
   knownr_make_and :> MakeAnd P Q PQ.
 Global Arguments KnownRMakeAnd {_ _} _%I _%I _%I.
 Global Hint Mode KnownRMakeAnd - + - ! - : typeclass_instances.
 
-Class MakeOr {SI} {PROP : bi SI} (P Q PQ : PROP) := make_or_l : P ∨ Q ⊣⊢ PQ.
+Class MakeOr `{SI: indexT} {PROP : bi} (P Q PQ : PROP) := make_or_l : P ∨ Q ⊣⊢ PQ.
 Global Arguments MakeOr {_ _} _%I _%I _%I.
 Global Hint Mode MakeOr - + - - - : typeclass_instances.
-Class KnownLMakeOr {SI} {PROP : bi SI} (P Q PQ : PROP) :=
+Class KnownLMakeOr `{SI: indexT} {PROP : bi} (P Q PQ : PROP) :=
   knownl_make_or :> MakeOr P Q PQ.
 Global Arguments KnownLMakeOr {_ _} _%I _%I _%I.
 Global Hint Mode KnownLMakeOr - + ! - - : typeclass_instances.
-Class KnownRMakeOr {SI} {PROP : bi SI} (P Q PQ : PROP) := knownr_make_or :> MakeOr P Q PQ.
+Class KnownRMakeOr `{SI: indexT} {PROP : bi} (P Q PQ : PROP) := knownr_make_or :> MakeOr P Q PQ.
 Global Arguments KnownRMakeOr {_ _} _%I _%I _%I.
 Global Hint Mode KnownRMakeOr - + - ! - : typeclass_instances.
 
-Class MakeAffinely {SI} {PROP : bi SI} (P Q : PROP) :=
+Class MakeAffinely `{SI: indexT} {PROP : bi} (P Q : PROP) :=
   make_affinely : <affine> P ⊣⊢ Q.
 Global Arguments MakeAffinely {_ _} _%I _%I.
 Global Hint Mode MakeAffinely - + - - : typeclass_instances.
-Class KnownMakeAffinely {SI} {PROP : bi SI} (P Q : PROP) :=
+Class KnownMakeAffinely `{SI: indexT} {PROP : bi} (P Q : PROP) :=
   known_make_affinely :> MakeAffinely P Q.
 Global Arguments KnownMakeAffinely {_ _} _%I _%I.
 Global Hint Mode KnownMakeAffinely - + ! - : typeclass_instances.
 
-Class MakeIntuitionistically {SI} {PROP : bi SI} (P Q : PROP) :=
+Class MakeIntuitionistically `{SI: indexT} {PROP : bi} (P Q : PROP) :=
   make_intuitionistically : □ P ⊣⊢ Q.
 Global Arguments MakeIntuitionistically {_ _} _%I _%I.
 Global Hint Mode MakeIntuitionistically - + - - : typeclass_instances.
-Class KnownMakeIntuitionistically {SI} {PROP : bi SI} (P Q : PROP) :=
+Class KnownMakeIntuitionistically `{SI: indexT} {PROP : bi} (P Q : PROP) :=
   known_make_intuitionistically :> MakeIntuitionistically P Q.
 Global Arguments KnownMakeIntuitionistically {_ _} _%I _%I.
 Global Hint Mode KnownMakeIntuitionistically - + ! - : typeclass_instances.
 
-Class MakeAbsorbingly {SI} {PROP : bi SI} (P Q : PROP) :=
+Class MakeAbsorbingly `{SI: indexT} {PROP : bi} (P Q : PROP) :=
   make_absorbingly : <absorb> P ⊣⊢ Q.
 Global Arguments MakeAbsorbingly {_ _} _%I _%I.
 Global Hint Mode MakeAbsorbingly - + - - : typeclass_instances.
-Class KnownMakeAbsorbingly {SI} {PROP : bi SI} (P Q : PROP) :=
+Class KnownMakeAbsorbingly `{SI: indexT} {PROP : bi} (P Q : PROP) :=
   known_make_absorbingly :> MakeAbsorbingly P Q.
 Global Arguments KnownMakeAbsorbingly {_ _} _%I _%I.
 Global Hint Mode KnownMakeAbsorbingly - + ! - : typeclass_instances.
 
-Class MakePersistently {SI} {PROP : bi SI} (P Q : PROP) :=
+Class MakePersistently `{SI: indexT} {PROP : bi} (P Q : PROP) :=
   make_persistently : <pers> P ⊣⊢ Q.
 Global Arguments MakePersistently {_ _} _%I _%I.
 Global Hint Mode MakePersistently - + - - : typeclass_instances.
-Class KnownMakePersistently {SI} {PROP : bi SI} (P Q : PROP) :=
+Class KnownMakePersistently `{SI: indexT} {PROP : bi} (P Q : PROP) :=
   known_make_persistently :> MakePersistently P Q.
 Global Arguments KnownMakePersistently {_ _} _%I _%I.
 Global Hint Mode KnownMakePersistently - + ! - : typeclass_instances.
 
-Class MakeLaterN {SI} {PROP : bi SI} (n : nat) (P lP : PROP) :=
+Class MakeLaterN `{SI: indexT} {PROP : bi} (n : nat) (P lP : PROP) :=
   make_laterN : ▷^n P ⊣⊢ lP.
 Global Arguments MakeLaterN {_ _} _%nat _%I _%I.
 Global Hint Mode MakeLaterN - + + - - : typeclass_instances.
-Class KnownMakeLaterN {SI} {PROP : bi SI} (n : nat) (P lP : PROP) :=
+Class KnownMakeLaterN `{SI: indexT} {PROP : bi} (n : nat) (P lP : PROP) :=
   known_make_laterN :> MakeLaterN n P lP.
 Global Arguments KnownMakeLaterN {_ _} _%nat _%I _%I.
 Global Hint Mode KnownMakeLaterN - + + ! - : typeclass_instances.
 
-Class MakeExcept0 {SI} {PROP : bi SI} (P Q : PROP) :=
+Class MakeExcept0 `{SI: indexT} {PROP : bi} (P Q : PROP) :=
   make_except_0 : ◇ P ⊣⊢ Q.
 Global Arguments MakeExcept0 {_ _} _%I _%I.
 Global Hint Mode MakeExcept0 - + - - : typeclass_instances.
-Class KnownMakeExcept0 {SI} {PROP : bi SI} (P Q : PROP) :=
+Class KnownMakeExcept0 `{SI: indexT} {PROP : bi} (P Q : PROP) :=
   known_make_except_0 :> MakeExcept0 P Q.
 Global Arguments KnownMakeExcept0 {_ _} _%I _%I.
 Global Hint Mode KnownMakeExcept0 - + ! - : typeclass_instances.
 
-Class IntoExcept0 {SI} {PROP : bi SI} (P Q : PROP) := into_except_0 : P ⊢ ◇ Q.
+Class IntoExcept0 `{SI: indexT} {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 Hint Mode IntoExcept0 - + ! - : typeclass_instances.
@@ -450,24 +450,24 @@ Lemma test_iFrame_later_1 P Q : P ∗ ▷ Q -∗ ▷ (P ∗ ▷ Q).
 Proof. iIntros "H". iFrame "H". Qed.
 >>
 *)
-Class MaybeIntoLaterN {SI} {PROP : bi SI} (only_head : bool) (n : nat) (P Q : PROP) :=
+Class MaybeIntoLaterN `{SI: indexT} {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 Hint Mode MaybeIntoLaterN - + + + - - : typeclass_instances.
 
-Class IntoLaterN {SI} {PROP : bi SI} (only_head : bool) (n : nat) (P Q : PROP) :=
+Class IntoLaterN `{SI: indexT} {PROP : bi} (only_head : bool) (n : nat) (P Q : PROP) :=
   into_laterN :> MaybeIntoLaterN only_head n P Q.
 Global Arguments IntoLaterN {_ _} _ _%nat_scope _%I _%I.
 Global Hint Mode IntoLaterN - + + + ! - : typeclass_instances.
 
-Global Instance maybe_into_laterN_default {SI} {PROP : bi SI} only_head n (P : PROP) :
+Global Instance maybe_into_laterN_default `{SI: indexT} {PROP : bi} only_head n (P : PROP) :
   MaybeIntoLaterN only_head n P P | 1000.
 Proof. apply laterN_intro. Qed.
 (* In the case both parameters are evars and n=0, we have to stop the
    search and unify both evars immediately instead of looping using
    other instances. *)
-Global Instance maybe_into_laterN_default_0 {SI} {PROP : bi SI} only_head (P : PROP) :
+Global Instance maybe_into_laterN_default_0 `{SI: indexT} {PROP : bi} only_head (P : PROP) :
   MaybeIntoLaterN only_head 0 P P | 0.
 Proof. apply _. Qed.
 
@@ -475,7 +475,7 @@ Proof. apply _. Qed.
 embeddings using [iModIntro].
 
 Input: the proposition [P], output: the proposition [Q] so that [P ⊢ ⎡Q⎤]. *)
-Class IntoEmbed {SI} {PROP PROP' : bi SI} `{BiEmbed SI PROP PROP'} (P : PROP') (Q : PROP) :=
+Class IntoEmbed `{SI: indexT} {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 {_}.
@@ -493,24 +493,24 @@ Global Hint Mode IntoEmbed - + + + ! -  : typeclass_instances.
    No Hint Modes are declared here. The appropriate one would be
    [Hint Mode - - ! -], but the fact that Coq ignores primitive
    projections for hints modes would make this fail.*)
-Class AsEmpValid {SI} {PROP : bi SI} (φ : Prop) (P : PROP) :=
+Class AsEmpValid `{SI: indexT} {PROP : bi} (φ : Prop) (P : PROP) :=
   as_emp_valid : φ ↔ ⊢ P.
 Global Arguments AsEmpValid {_ _} _%type _%I.
-Class AsEmpValid0 {SI} {PROP : bi SI} (φ : Prop) (P : PROP) :=
+Class AsEmpValid0 `{SI: indexT} {PROP : bi} (φ : Prop) (P : PROP) :=
   as_emp_valid_0 : AsEmpValid φ P.
 Global Arguments AsEmpValid0 {_ _} _%type _%I.
-Existing Instance as_emp_valid_0 | 0.
+Global Existing Instance as_emp_valid_0 | 0.
 
-Lemma as_emp_valid_1 (φ : Prop) {SI} {PROP : bi SI} (P : PROP) `{!AsEmpValid φ P} :
+Lemma as_emp_valid_1 (φ : Prop) `{SI: indexT} {PROP : bi} (P : PROP) `{!AsEmpValid φ P} :
   φ → ⊢ P.
 Proof. by apply as_emp_valid. Qed.
-Lemma as_emp_valid_2 (φ : Prop) {SI} {PROP : bi SI} (P : PROP) `{!AsEmpValid φ P} :
+Lemma as_emp_valid_2 (φ : Prop) `{SI: indexT} {PROP : bi} (P : PROP) `{!AsEmpValid φ P} :
   (⊢ P) → φ.
 Proof. by apply as_emp_valid. Qed.
 
 (* Input: [P]; Outputs: [N],
    Extracts the namespace associated with an invariant assertion. Used for [iInv]. *)
-Class IntoInv {SI} {PROP : bi SI} (P: PROP) (N: namespace).
+Class IntoInv `{SI: indexT} {PROP : bi} (P: PROP) (N: namespace).
 Global Arguments IntoInv {_ _} _%I _.
 Global Hint Mode IntoInv - + ! - : typeclass_instances.
 
@@ -519,7 +519,7 @@ Global Hint Mode IntoInv - + ! - : typeclass_instances.
     usable and general form would use telescopes and also allow binders for the
     closing view shift.  [γ] is an [option] to make it easy for ElimAcc
     instances to recognize the [emp] case and make it look nicer. *)
-Definition accessor {SI} {PROP : bi SI} {X : Type} (M1 M2 : PROP → PROP)
+Definition accessor `{SI: indexT} {PROP : bi} {X : Type} (M1 M2 : PROP → PROP)
            (α β : X → PROP) (mγ : X → option PROP) : PROP :=
   M1 (∃ x, α x ∗ (β x -∗ M2 (default emp (mγ x))))%I.
 
@@ -530,7 +530,7 @@ Definition accessor {SI} {PROP : bi SI} {X : Type} (M1 M2 : PROP → PROP)
    Elliminates an accessor [accessor E1 E2 α β γ] in goal [Q'], turning the goal
    into [Q'] with a new assumption [α x], where [φ] is a side-condition at the
    Cow level that needs to hold. *)
-Class ElimAcc {SI} {PROP : bi SI} {X : Type} (φ : Prop) (M1 M2 : PROP → PROP)
+Class ElimAcc `{SI: indexT} {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).
@@ -548,7 +548,7 @@ Global Hint Mode ElimAcc - + ! - ! ! ! ! ! ! - : typeclass_instances.
    - [M1], [M2]: the two accessor modalities (they will typically still have
      some evars though, e.g. for the masks)
 *)
-Class IntoAcc {SI} {PROP : bi SI} {X : Type} (Pacc : PROP) (φ : Prop) (Pin : PROP)
+Class IntoAcc `{SI: indexT} {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.
@@ -575,7 +575,7 @@ Global Hint Mode IntoAcc - + - ! - - - - - - - : typeclass_instances.
 
    TODO: Add support for a binder (like accessors have it).
 *)
-Class ElimInv {SI} {PROP : bi SI} {X : Type} (φ : Prop)
+Class ElimInv `{SI: indexT} {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.
@@ -599,40 +599,40 @@ with the exception of:
 - [MaybeIntoLaterN] and [FromLaterN] used by [iNext]
 - [IntoPersistent] used by [iIntuitionistic]
 *)
-Global Instance into_pure_tc_opaque {SI} {PROP : bi SI} (P : PROP) φ :
+Global Instance into_pure_tc_opaque `{SI: indexT} {PROP : bi} (P : PROP) φ :
   IntoPure P φ → IntoPure (tc_opaque P) φ := id.
-Global Instance from_pure_tc_opaque {SI} {PROP : bi SI} (a : bool) (P : PROP) φ :
+Global Instance from_pure_tc_opaque `{SI: indexT} {PROP : bi} (a : bool) (P : PROP) φ :
   FromPure a P φ → FromPure a (tc_opaque P) φ := id.
-Global Instance from_wand_tc_opaque {SI} {PROP : bi SI} (P Q1 Q2 : PROP) :
+Global Instance from_wand_tc_opaque `{SI: indexT} {PROP : bi} (P Q1 Q2 : PROP) :
   FromWand P Q1 Q2 → FromWand (tc_opaque P) Q1 Q2 := id.
-Global Instance into_wand_tc_opaque {SI} {PROP : bi SI} p q (R P Q : PROP) :
+Global Instance into_wand_tc_opaque `{SI: indexT} {PROP : bi} p q (R P Q : PROP) :
   IntoWand p q R P Q → IntoWand p q (tc_opaque R) P Q := id.
 (* Higher precedence than [from_and_sep] so that [iCombine] does not loop. *)
-Global Instance from_and_tc_opaque {SI} {PROP : bi SI} (P Q1 Q2 : PROP) :
+Global Instance from_and_tc_opaque `{SI: indexT} {PROP : bi} (P Q1 Q2 : PROP) :
   FromAnd P Q1 Q2 → FromAnd (tc_opaque P) Q1 Q2 | 102 := id.
-Global Instance into_and_tc_opaque {SI} {PROP : bi SI} p (P Q1 Q2 : PROP) :
+Global Instance into_and_tc_opaque `{SI: indexT} {PROP : bi} p (P Q1 Q2 : PROP) :
   IntoAnd p P Q1 Q2 → IntoAnd p (tc_opaque P) Q1 Q2 := id.
-Global Instance into_sep_tc_opaque {SI} {PROP : bi SI} (P Q1 Q2 : PROP) :
+Global Instance into_sep_tc_opaque `{SI: indexT} {PROP : bi} (P Q1 Q2 : PROP) :
   IntoSep P Q1 Q2 → IntoSep (tc_opaque P) Q1 Q2 := id.
-Global Instance from_or_tc_opaque {SI} {PROP : bi SI} (P Q1 Q2 : PROP) :
+Global Instance from_or_tc_opaque `{SI: indexT} {PROP : bi} (P Q1 Q2 : PROP) :
   FromOr P Q1 Q2 → FromOr (tc_opaque P) Q1 Q2 := id.
-Global Instance into_or_tc_opaque {SI} {PROP : bi SI} (P Q1 Q2 : PROP) :
+Global Instance into_or_tc_opaque `{SI: indexT} {PROP : bi} (P Q1 Q2 : PROP) :
   IntoOr P Q1 Q2 → IntoOr (tc_opaque P) Q1 Q2 := id.
-Global Instance from_exist_tc_opaque {SI} {PROP : bi SI} {A} (P : PROP) (Φ : A → PROP) :
+Global Instance from_exist_tc_opaque `{SI: indexT} {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
   FromExist P Φ → FromExist (tc_opaque P) Φ := id.
-Global Instance into_exist_tc_opaque {SI} {PROP : bi SI} {A} (P : PROP) (Φ : A → PROP) (name: ident_name) :
+Global Instance into_exist_tc_opaque `{SI: indexT} {PROP : bi} {A} (P : PROP) (Φ : A → PROP) (name: ident_name) :
   IntoExist P Φ name → IntoExist (tc_opaque P) Φ name := id.
-Global Instance from_forall_tc_opaque {SI} {PROP : bi SI} {A} (P : PROP) (Φ : A → PROP) (name : ident_name) :
+Global Instance from_forall_tc_opaque `{SI: indexT} {PROP : bi} {A} (P : PROP) (Φ : A → PROP) (name : ident_name) :
   FromForall P Φ name → FromForall (tc_opaque P) Φ name := id.
-Global Instance into_forall_tc_opaque {SI} {PROP : bi SI} {A} (P : PROP) (Φ : A → PROP) :
+Global Instance into_forall_tc_opaque `{SI: indexT} {PROP : bi} {A} (P : PROP) (Φ : A → PROP) :
   IntoForall P Φ → IntoForall (tc_opaque P) Φ := id.
-Global Instance from_modal_tc_opaque {SI} {PROP1 PROP2 : bi SI} {A}
+Global Instance from_modal_tc_opaque `{SI: indexT} {PROP1 PROP2 : bi} {A}
     M (sel : A) (P : PROP2) (Q : PROP1) :
   FromModal M sel P Q → FromModal M sel (tc_opaque P) Q := id.
-Global Instance elim_modal_tc_opaque {SI} {PROP : bi SI} φ p p' (P P' Q Q' : PROP) :
+Global Instance elim_modal_tc_opaque `{SI: indexT} {PROP : bi} φ p p' (P P' Q Q' : PROP) :
   ElimModal φ p p' P P' Q Q' → ElimModal φ p p' (tc_opaque P) P' Q Q' := id.
-Global Instance into_inv_tc_opaque {SI} {PROP : bi SI} (P : PROP) N :
+Global Instance into_inv_tc_opaque `{SI: indexT} {PROP : bi} (P : PROP) N :
   IntoInv P N → IntoInv (tc_opaque P) N := id.
-Global Instance elim_inv_tc_opaque {SI} {PROP : bi SI} {X} φ Pinv Pin Pout Pclose Q Q' :
+Global Instance elim_inv_tc_opaque `{SI: indexT} {PROP : bi} {X} φ Pinv Pin Pout Pclose Q Q' :
   ElimInv (PROP:=PROP) (X:=X) φ Pinv Pin Pout Pclose Q Q' →
   ElimInv φ (tc_opaque Pinv) Pin Pout Pclose Q Q' := id.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 4ef75d32c1fe791e1f096dbd222975f093aedff5..1ff7d2aafa20410822c27bb297ec5f322b1c1ab2 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -8,7 +8,7 @@ Local Open Scope lazy_bool_scope.
 
 (* Coq versions of the tactics *)
 Section tactics.
-Context {SI} {PROP : bi SI}.
+Context `{SI: indexT} {PROP : bi}.
 Implicit Types Γ : env PROP.
 Implicit Types Δ : envs PROP.
 Implicit Types P Q : PROP.
@@ -573,7 +573,7 @@ Proof.
 Qed.
 
 (** * Combining *)
-Class FromSeps {SI} {PROP : bi SI} (P : PROP) (Qs : list PROP) :=
+Class FromSeps `{SI: indexT} {PROP : bi} (P : PROP) (Qs : list PROP) :=
   from_seps : [∗] Qs ⊢ P.
 Local Arguments FromSeps {_ _} _%I _%I.
 Local Arguments from_seps {_ _} _%I _%I {_}.
@@ -799,7 +799,7 @@ Qed.
 (** * Rewriting *)
 Lemma tac_rewrite `{!BiInternalEq PROP} Δ i p Pxy d Q :
   envs_lookup i Δ = Some (p, Pxy) →
-  ∀ {A : ofe SI} (x y : A) (Φ : A → PROP),
+  ∀ {A : ofe} (x y : A) (Φ : A → PROP),
     IntoInternalEq Pxy x y →
     (Q ⊣⊢ Φ (if d is Left then y else x)) →
     NonExpansive Φ →
@@ -814,7 +814,7 @@ Qed.
 Lemma tac_rewrite_in `{!BiInternalEq PROP} Δ i p Pxy j q P d Q :
   envs_lookup i Δ = Some (p, Pxy) →
   envs_lookup j Δ = Some (q, P) →
-  ∀ {A : ofe SI} (x y : A) (Φ : A → PROP),
+  ∀ {A : ofe} (x y : A) (Φ : A → PROP),
     IntoInternalEq Pxy x y →
     (P ⊣⊢ Φ (if d is Left then y else x)) →
     NonExpansive Φ →
@@ -870,7 +870,7 @@ Inputs:
 
 Outputs:
 - [Γout] : the resulting environment. *)
-Class TransformIntuitionisticEnv {SI} {PROP1 PROP2: bi SI} (M : modality PROP1 PROP2)
+Class TransformIntuitionisticEnv {SI: indexT} {PROP1 PROP2: bi} (M : modality PROP1 PROP2)
     (C : PROP2 → PROP1 → Prop) (Γin : env PROP2) (Γout : env PROP1) := {
   transform_intuitionistic_env :
     (∀ P Q, C P Q → □ P ⊢ M (□ Q)) →
@@ -893,7 +893,7 @@ Inputs:
 Outputs:
 - [Γout] : the resulting environment.
 - [filtered] : a Boolean indicating if non-affine hypotheses have been cleared. *)
-Class TransformSpatialEnv {SI} {PROP1 PROP2: bi SI} (M : modality PROP1 PROP2)
+Class TransformSpatialEnv {SI: indexT} {PROP1 PROP2: bi} (M : modality PROP1 PROP2)
     (C : PROP2 → PROP1 → Prop) (Γin : env PROP2) (Γout : env PROP1)
     (filtered : bool) := {
   transform_spatial_env :
@@ -915,7 +915,7 @@ Inputs:
 
 Outputs:
 - [Γout] : the resulting environment. *)
-Inductive IntoModalIntuitionisticEnv {SI} {PROP2: bi SI} : ∀ {PROP1} (M : modality PROP1 PROP2)
+Inductive IntoModalIntuitionisticEnv {SI: indexT} {PROP2: bi} : ∀ {PROP1} (M : modality PROP1 PROP2)
     (Γin : env PROP2) (Γout : env PROP1), modality_action PROP1 PROP2 → Prop :=
   | MIEnvIsEmpty_intuitionistic {PROP1} (M : modality PROP1 PROP2) :
      IntoModalIntuitionisticEnv M Enil Enil MIEnvIsEmpty
@@ -926,12 +926,12 @@ Inductive IntoModalIntuitionisticEnv {SI} {PROP2: bi SI} : ∀ {PROP1} (M : moda
        (M : modality PROP1 PROP2) (C : PROP2 → PROP1 → Prop) Γin Γout :
      TransformIntuitionisticEnv M C Γin Γout →
      IntoModalIntuitionisticEnv M Γin Γout (MIEnvTransform C)
-  | MIEnvClear_intuitionistic {PROP1 : bi SI} (M : modality PROP1 PROP2) Γ :
+  | MIEnvClear_intuitionistic {PROP1 : bi} (M : modality PROP1 PROP2) Γ :
      IntoModalIntuitionisticEnv M Γ Enil MIEnvClear
   | MIEnvId_intuitionistic (M : modality PROP2 PROP2) Γ :
      IntoModalIntuitionisticEnv M Γ Γ MIEnvId.
 Existing Class IntoModalIntuitionisticEnv.
-Existing Instances MIEnvIsEmpty_intuitionistic MIEnvForall_intuitionistic
+Global Existing Instances MIEnvIsEmpty_intuitionistic MIEnvForall_intuitionistic
   MIEnvTransform_intuitionistic MIEnvClear_intuitionistic MIEnvId_intuitionistic.
 
 (* The class [IntoModalSpatialEnv M Γin Γout s] is used to transform the spatial
@@ -947,7 +947,7 @@ Inputs:
 Outputs:
 - [Γout] : the resulting environment.
 - [filtered] : a Boolean indicating if non-affine hypotheses have been cleared. *)
-Inductive IntoModalSpatialEnv {SI} {PROP2: bi SI} : ∀ {PROP1} (M : modality PROP1 PROP2)
+Inductive IntoModalSpatialEnv {SI: indexT} {PROP2: bi} : ∀ {PROP1} (M : modality PROP1 PROP2)
     (Γin : env PROP2) (Γout : env PROP1), modality_action PROP1 PROP2 → bool → Prop :=
   | MIEnvIsEmpty_spatial {PROP1} (M : modality PROP1 PROP2) :
      IntoModalSpatialEnv M Enil Enil MIEnvIsEmpty false
@@ -958,16 +958,16 @@ Inductive IntoModalSpatialEnv {SI} {PROP2: bi SI} : ∀ {PROP1} (M : modality PR
        (M : modality PROP1 PROP2) (C : PROP2 → PROP1 → Prop) Γin Γout fi :
      TransformSpatialEnv M C Γin Γout fi →
      IntoModalSpatialEnv M Γin Γout (MIEnvTransform C) fi
-  | MIEnvClear_spatial {PROP1 : bi SI} (M : modality PROP1 PROP2) Γ :
+  | MIEnvClear_spatial {PROP1 : bi} (M : modality PROP1 PROP2) Γ :
      IntoModalSpatialEnv M Γ Enil MIEnvClear false
   | MIEnvId_spatial (M : modality PROP2 PROP2) Γ :
      IntoModalSpatialEnv M Γ Γ MIEnvId false.
 Existing Class IntoModalSpatialEnv.
-Existing Instances MIEnvIsEmpty_spatial MIEnvForall_spatial
+Global Existing Instances MIEnvIsEmpty_spatial MIEnvForall_spatial
   MIEnvTransform_spatial MIEnvClear_spatial MIEnvId_spatial.
 
 Section tac_modal_intro.
-  Context {SI} {PROP1 PROP2 : bi SI} (M : modality PROP1 PROP2).
+  Context {SI: indexT} {PROP1 PROP2 : bi} (M : modality PROP1 PROP2).
 
   Global Instance transform_intuitionistic_env_nil C : TransformIntuitionisticEnv M C Enil Enil.
   Proof.
@@ -1079,7 +1079,7 @@ End tac_modal_intro.
 
 (** The class [MaybeIntoLaterNEnvs] is used by tactics that need to introduce
 laters, e.g., the symbolic execution tactics. *)
-Class MaybeIntoLaterNEnvs {SI} {PROP: bi SI} (n : nat) (Δ1 Δ2 : envs PROP) := {
+Class MaybeIntoLaterNEnvs {SI: indexT} {PROP: bi} (n : nat) (Δ1 Δ2 : envs PROP) := {
   into_later_intuitionistic :
     TransformIntuitionisticEnv (modality_laterN n) (MaybeIntoLaterN false n)
       (env_intuitionistic Δ1) (env_intuitionistic Δ2);
@@ -1088,13 +1088,13 @@ Class MaybeIntoLaterNEnvs {SI} {PROP: bi SI} (n : nat) (Δ1 Δ2 : envs PROP) :=
       (MaybeIntoLaterN false n) (env_spatial Δ1) (env_spatial Δ2) false
 }.
 
-Global Instance into_laterN_envs {SI} {PROP: bi SI} n (Γp1 Γp2 Γs1 Γs2 : env PROP) m :
+Global Instance into_laterN_envs {SI: indexT} {PROP: bi} n (Γp1 Γp2 Γs1 Γs2 : env PROP) m :
   TransformIntuitionisticEnv (modality_laterN n) (MaybeIntoLaterN false n) Γp1 Γp2 →
   TransformSpatialEnv (modality_laterN n) (MaybeIntoLaterN false n) Γs1 Γs2 false →
   MaybeIntoLaterNEnvs n (Envs Γp1 Γs1 m) (Envs Γp2 Γs2 m).
 Proof. by split. Qed.
 
-Lemma into_laterN_env_sound {SI} {PROP : bi SI} n (Δ1 Δ2 : envs PROP) :
+Lemma into_laterN_env_sound {SI: indexT} {PROP : bi} n (Δ1 Δ2 : envs PROP) :
   MaybeIntoLaterNEnvs n Δ1 Δ2 → of_envs Δ1 ⊢ ▷^n (of_envs Δ2).
 Proof.
   intros [[Hp ??] [Hs ??]]; rewrite !of_envs_eq /= !laterN_and -laterN_sep_2.
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index d2b1d3b38a02db8c18aad90eff41aeb065f6d830..339bbc97826990d694aedd859ab40634b62aaf0d 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -210,7 +210,7 @@ Global Instance env_to_list_subenv_proper :
 Proof. induction 1; simpl; constructor; auto. Qed.
 End env.
 
-Record envs {SI} (PROP : bi SI) := Envs {
+Record envs `{SI: indexT} (PROP : bi) := Envs {
   env_intuitionistic : env PROP;
   env_spatial : env PROP;
   env_counter : positive (** A counter to generate fresh hypothesis names *)
@@ -240,53 +240,53 @@ We first define a version [pre_envs_entails] that takes the two contexts
 [env_intuitionistic] and [env_spatial] as its arguments. We seal this definition
 and then lift it to take the whole proof mode context [Δ : envs PROP]. This is
 crucial to make sure that the counter [env_counter] is not part of the seal. *)
-Record envs_wf' {SI} {PROP : bi SI} (Γp Γs : env PROP) := {
+Record envs_wf' `{SI: indexT} {PROP : bi} (Γp Γs : env PROP) := {
   env_intuitionistic_valid : env_wf Γp;
   env_spatial_valid : env_wf Γs;
   envs_disjoint i : Γp !! i = None ∨ Γs !! i = None
 }.
-Definition envs_wf {SI} {PROP : bi SI} (Δ : envs PROP) :=
+Definition envs_wf `{SI: indexT} {PROP : bi} (Δ : envs PROP) :=
   envs_wf' (env_intuitionistic Δ) (env_spatial Δ).
 
-Definition of_envs' {SI} {PROP : bi SI} (Γp Γs : env PROP) : PROP :=
+Definition of_envs' `{SI: indexT} {PROP : bi} (Γp Γs : env PROP) : PROP :=
   (⌜envs_wf' Γp Γs⌝ ∧ □ [∧] Γp ∗ [∗] Γs)%I.
 Global Instance: Params (@of_envs') 2 := {}.
-Definition of_envs {SI} {PROP : bi SI} (Δ : envs PROP) : PROP :=
+Definition of_envs `{SI: indexT} {PROP : bi} (Δ : envs PROP) : PROP :=
   of_envs' (env_intuitionistic Δ) (env_spatial Δ).
 Global Instance: Params (@of_envs) 2 := {}.
 Global Arguments of_envs : simpl never.
 
-Definition pre_envs_entails_def {SI} {PROP : bi SI} (Γp Γs : env PROP) (Q : PROP) :=
+Definition pre_envs_entails_def `{SI: indexT} {PROP : bi} (Γp Γs : env PROP) (Q : PROP) :=
   of_envs' Γp Γs ⊢ Q.
 Definition pre_envs_entails_aux : seal (@pre_envs_entails_def). Proof. by eexists. Qed.
 Definition pre_envs_entails := pre_envs_entails_aux.(unseal).
 Definition pre_envs_entails_eq : @pre_envs_entails = @pre_envs_entails_def :=
   pre_envs_entails_aux.(seal_eq).
 
-Definition envs_entails {SI} {PROP : bi SI} (Δ : envs PROP) (Q : PROP) : Prop :=
+Definition envs_entails `{SI: indexT} {PROP : bi} (Δ : envs PROP) (Q : PROP) : Prop :=
   pre_envs_entails SI PROP (env_intuitionistic Δ) (env_spatial Δ) Q.
 Definition envs_entails_eq :
-  @envs_entails = λ SI (PROP: bi SI) (Δ : envs PROP) Q, (of_envs Δ ⊢ Q).
+  @envs_entails = λ SI (PROP: bi) (Δ : envs PROP) Q, (of_envs Δ ⊢ Q).
 Proof. by rewrite /envs_entails pre_envs_entails_eq. Qed.
 Global Arguments envs_entails {SI} {PROP} Δ Q%I.
 Global Instance: Params (@envs_entails) 2 := {}.
 
-Record envs_Forall2 {SI} {PROP : bi SI} (R : relation PROP) (Δ1 Δ2 : envs PROP) := {
+Record envs_Forall2 `{SI: indexT} {PROP : bi} (R : relation PROP) (Δ1 Δ2 : envs PROP) := {
   env_intuitionistic_Forall2 : env_Forall2 R (env_intuitionistic Δ1) (env_intuitionistic Δ2);
   env_spatial_Forall2 : env_Forall2 R (env_spatial Δ1) (env_spatial Δ2)
 }.
 
-Definition envs_dom {SI} {PROP: bi SI} (Δ : envs PROP) : list ident :=
+Definition envs_dom `{SI: indexT} {PROP: bi} (Δ : envs PROP) : list ident :=
   env_dom (env_intuitionistic Δ) ++ env_dom (env_spatial Δ).
 
-Definition envs_lookup {SI} {PROP: bi SI} (i : ident) (Δ : envs PROP) : option (bool * PROP) :=
+Definition envs_lookup `{SI: indexT} {PROP: bi} (i : ident) (Δ : envs PROP) : option (bool * PROP) :=
   let (Γp,Γs,n) := Δ in
   match env_lookup i Γp with
   | Some P => Some (true, P)
   | None => P ← env_lookup i Γs; Some (false, P)
   end.
 
-Definition envs_delete {SI} {PROP: bi SI} (remove_intuitionistic : bool)
+Definition envs_delete `{SI: indexT} {PROP: bi} (remove_intuitionistic : bool)
     (i : ident) (p : bool) (Δ : envs PROP) : envs PROP :=
   let (Γp,Γs,n) := Δ in
   match p with
@@ -294,7 +294,7 @@ Definition envs_delete {SI} {PROP: bi SI} (remove_intuitionistic : bool)
   | false => Envs Γp (env_delete i Γs) n
   end.
 
-Definition envs_lookup_delete {SI} {PROP: bi SI} (remove_intuitionistic : bool)
+Definition envs_lookup_delete `{SI: indexT} {PROP: bi} (remove_intuitionistic : bool)
     (i : ident) (Δ : envs PROP) : option (bool * PROP * envs PROP) :=
   let (Γp,Γs,n) := Δ in
   match env_lookup_delete i Γp with
@@ -302,7 +302,7 @@ Definition envs_lookup_delete {SI} {PROP: bi SI} (remove_intuitionistic : bool)
   | None => '(P,Γs') ← env_lookup_delete i Γs; Some (false, P, Envs Γp Γs' n)
   end.
 
-Fixpoint envs_lookup_delete_list {SI} {PROP: bi SI} (remove_intuitionistic : bool)
+Fixpoint envs_lookup_delete_list `{SI: indexT} {PROP: bi} (remove_intuitionistic : bool)
     (js : list ident) (Δ : envs PROP) : option (bool * list PROP * envs PROP) :=
   match js with
   | [] => Some (true, [], Δ)
@@ -312,12 +312,12 @@ Fixpoint envs_lookup_delete_list {SI} {PROP: bi SI} (remove_intuitionistic : boo
      Some ((p:bool) &&& q, P :: Ps, Δ'')
   end.
 
-Definition envs_snoc {SI} {PROP: bi SI} (Δ : envs PROP)
+Definition envs_snoc `{SI: indexT} {PROP: bi} (Δ : envs PROP)
     (p : bool) (j : ident) (P : PROP) : envs PROP :=
   let (Γp,Γs,n) := Δ in
   if p then Envs (Esnoc Γp j P) Γs n else Envs Γp (Esnoc Γs j P) n.
 
-Definition envs_app {SI} {PROP: bi SI} (p : bool)
+Definition envs_app `{SI: indexT} {PROP: bi} (p : bool)
     (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
   let (Γp,Γs,n) := Δ in
   match p with
@@ -325,7 +325,7 @@ Definition envs_app {SI} {PROP: bi SI} (p : bool)
   | false => _ ← env_app Γ Γp; Γs' ← env_app Γ Γs; Some (Envs Γp Γs' n)
   end.
 
-Definition envs_simple_replace {SI} {PROP: bi SI} (i : ident) (p : bool)
+Definition envs_simple_replace `{SI: indexT} {PROP: bi} (i : ident) (p : bool)
     (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
   let (Γp,Γs,n) := Δ in
   match p with
@@ -333,24 +333,24 @@ Definition envs_simple_replace {SI} {PROP: bi SI} (i : ident) (p : bool)
   | false => _ ← env_app Γ Γp; Γs' ← env_replace i Γ Γs; Some (Envs Γp Γs' n)
   end.
 
-Definition envs_replace {SI} {PROP: bi SI} (i : ident) (p q : bool)
+Definition envs_replace `{SI: indexT} {PROP: bi} (i : ident) (p q : bool)
     (Γ : env PROP) (Δ : envs PROP) : option (envs PROP) :=
   if beq p q then envs_simple_replace i p Γ Δ
   else envs_app q Γ (envs_delete true i p Δ).
 
-Definition env_spatial_is_nil {SI} {PROP: bi SI} (Δ : envs PROP) : bool :=
+Definition env_spatial_is_nil `{SI: indexT} {PROP: bi} (Δ : envs PROP) : bool :=
   if env_spatial Δ is Enil then true else false.
 
-Definition envs_clear_spatial {SI} {PROP: bi SI} (Δ : envs PROP) : envs PROP :=
+Definition envs_clear_spatial `{SI: indexT} {PROP: bi} (Δ : envs PROP) : envs PROP :=
   Envs (env_intuitionistic Δ) Enil (env_counter Δ).
 
-Definition envs_clear_intuitionistic {SI} {PROP: bi SI} (Δ : envs PROP) : envs PROP :=
+Definition envs_clear_intuitionistic `{SI: indexT} {PROP: bi} (Δ : envs PROP) : envs PROP :=
   Envs Enil (env_spatial Δ) (env_counter Δ).
 
-Definition envs_incr_counter {SI} {PROP: bi SI} (Δ : envs PROP) : envs PROP :=
+Definition envs_incr_counter `{SI: indexT} {PROP: bi} (Δ : envs PROP) : envs PROP :=
   Envs (env_intuitionistic Δ) (env_spatial Δ) (Pos_succ (env_counter Δ)).
 
-Fixpoint envs_split_go {SI} {PROP: bi SI}
+Fixpoint envs_split_go `{SI: indexT} {PROP: bi}
     (js : list ident) (Δ1 Δ2 : envs PROP) : option (envs PROP * envs PROP) :=
   match js with
   | [] => Some (Δ1, Δ2)
@@ -361,23 +361,23 @@ Fixpoint envs_split_go {SI} {PROP: bi SI}
   end.
 (* if [d = Right] then [result = (remaining hyps, hyps named js)] and
    if [d = Left] then [result = (hyps named js, remaining hyps)] *)
-Definition envs_split {SI} {PROP: bi SI} (d : direction)
+Definition envs_split `{SI: indexT} {PROP: bi} (d : direction)
     (js : list ident) (Δ : envs PROP) : option (envs PROP * envs PROP) :=
   '(Δ1,Δ2) ← envs_split_go js Δ (envs_clear_spatial Δ);
   if d is Right then Some (Δ1,Δ2) else Some (Δ2,Δ1).
 
-Fixpoint env_to_prop_go {SI} {PROP : bi SI} (acc : PROP) (Γ : env PROP) : PROP :=
+Fixpoint env_to_prop_go `{SI: indexT} {PROP : bi} (acc : PROP) (Γ : env PROP) : PROP :=
   match Γ with Enil => acc | Esnoc Γ _ P => env_to_prop_go (P ∗ acc)%I Γ end.
-Definition env_to_prop {SI} {PROP : bi SI} (Γ : env PROP) : PROP :=
+Definition env_to_prop `{SI: indexT} {PROP : bi} (Γ : env PROP) : PROP :=
   match Γ with Enil => emp%I | Esnoc Γ _ P => env_to_prop_go P Γ end.
 
-Fixpoint env_to_prop_and_go {SI} {PROP : bi SI} (acc : PROP) (Γ : env PROP) : PROP :=
+Fixpoint env_to_prop_and_go `{SI: indexT} {PROP : bi} (acc : PROP) (Γ : env PROP) : PROP :=
   match Γ with Enil => acc | Esnoc Γ _ P => env_to_prop_and_go (P ∧ acc)%I Γ end.
-Definition env_to_prop_and {SI} {PROP : bi SI} (Γ : env PROP) : PROP :=
+Definition env_to_prop_and `{SI: indexT} {PROP : bi} (Γ : env PROP) : PROP :=
   match Γ with Enil => True%I | Esnoc Γ _ P => env_to_prop_and_go P Γ end.
 
 Section envs.
-Context {SI} {PROP : bi SI}.
+Context `{SI: indexT} {PROP : bi}.
 Implicit Types Γ Γp Γs : env PROP.
 Implicit Types Δ : envs PROP.
 Implicit Types P Q : PROP.
diff --git a/theories/proofmode/frame_instances.v b/theories/proofmode/frame_instances.v
index 37aadb596ccfac31138dece993b03d3ba55ae310..f4da9ba46e2d5443e53a2344f63f38a2d0916929 100644
--- a/theories/proofmode/frame_instances.v
+++ b/theories/proofmode/frame_instances.v
@@ -16,7 +16,7 @@ but that makes framing less predictable and might have some performance impact.
 Hence, we only perform such cleanup for [True] and [emp]. *)
 
 Section bi.
-Context {SI} {PROP : bi SI}.
+Context `{SI: indexT} {PROP : bi}.
 Implicit Types P Q R : PROP.
 (* Frame *)
 Global Instance frame_here_absorbing p R : Absorbing R → Frame p R R True | 0.
@@ -51,23 +51,23 @@ Proof.
   - by rewrite right_id -affinely_affinely_if affine_affinely.
 Qed.
 
-Global Instance make_embed_pure `{BiEmbed SI PROP PROP'} φ :
+Global Instance make_embed_pure `{!BiEmbed PROP PROP'} φ :
   KnownMakeEmbed (PROP:=PROP) ⌜φ⌝ ⌜φ⌝.
 Proof. apply embed_pure. Qed.
-Global Instance make_embed_emp `{BiEmbedEmp SI PROP PROP'} :
+Global Instance make_embed_emp `{!BiEmbed PROP PROP'} `{!BiEmbedEmp PROP PROP'} :
   KnownMakeEmbed (PROP:=PROP) emp emp.
 Proof. apply embed_emp. Qed.
-Global Instance make_embed_default `{BiEmbed SI PROP PROP'} P :
+Global Instance make_embed_default `{!BiEmbed PROP PROP'} P :
   MakeEmbed P (⎡P⎤)%I | 100.
 Proof. by rewrite /MakeEmbed. Qed.
 
-Global Instance frame_embed `{BiEmbed SI PROP PROP'} p P Q (Q' : PROP') R :
+Global Instance frame_embed `{!BiEmbed PROP PROP'} p P Q (Q' : PROP') R :
   Frame p R P Q → MakeEmbed Q Q' → Frame p ⎡R⎤ ⎡P⎤ Q'.
 Proof.
   rewrite /Frame /MakeEmbed => <- <-.
   rewrite embed_sep embed_intuitionistically_if_2 => //.
 Qed.
-Global Instance frame_pure_embed `{BiEmbed SI PROP PROP'} p P Q (Q' : PROP') φ :
+Global Instance frame_pure_embed `{!BiEmbed PROP PROP'} p P Q (Q' : PROP') φ :
   Frame p ⌜φ⌝ P Q → MakeEmbed Q Q' → Frame p ⌜φ⌝ ⎡P⎤ Q'.
 Proof. rewrite /Frame /MakeEmbed -embed_pure. apply (frame_embed p P Q). Qed.
 
@@ -302,9 +302,9 @@ Proof.
   rewrite persistently_elim impl_elim_r //.
 Qed.
 
-Global Instance frame_eq_embed {PROP': bi SI} `{!BiEmbed PROP PROP', !BiInternalEq PROP,
+Global Instance frame_eq_embed {PROP': bi} `{!BiEmbed PROP PROP', !BiInternalEq PROP,
     !BiInternalEq PROP', !BiEmbedInternalEq PROP PROP'}
-    p P Q (Q' : PROP') {A : ofe SI} (a b : A) :
+    p P Q (Q' : PROP') {A : ofe} (a b : A) :
   Frame p (a ≡ b) P Q → MakeEmbed Q Q' → Frame p (a ≡ b) ⎡P⎤ Q'.
 Proof. rewrite /Frame /MakeEmbed -embed_internal_eq. apply (frame_embed p P Q). Qed.
 
@@ -331,10 +331,10 @@ Proof.
   by rewrite laterN_intuitionistically_if_2 laterN_sep_2.
 Qed.
 
-Global Instance frame_bupd `{BiBUpd SI PROP} p R P Q :
+Global Instance frame_bupd `{!BiBUpd PROP} p R P Q :
   Frame p R P Q → Frame p R (|==> P) (|==> Q).
 Proof. rewrite /Frame=><-. by rewrite bupd_frame_l. Qed.
-Global Instance frame_fupd `{BiFUpd SI PROP} p E1 E2 R P Q :
+Global Instance frame_fupd `{!BiFUpd PROP} p E1 E2 R P Q :
   Frame p R P Q → Frame p R (|={E1,E2}=> P) (|={E1,E2}=> Q).
 Proof. rewrite /Frame=><-. by rewrite fupd_frame_l. Qed.
 
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 1fb925dccf38d7156c332d5287f8153d83bbe164..e92fbea65b7d6beedfaaa057963968c015b00f13 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1039,7 +1039,7 @@ returns [false], then the conclusion can be moved in the intuitionistic context
 even if conditions 1 and 3 do not hold. Therefore, in that case, we prefer
 putting the conclusion to the intuitionistic context directly and not using
 [tac_specialize_intuitionistic_helper], which requires conditions 1 and 3. *)
-Fixpoint use_tac_specialize_intuitionistic_helper {SI} {M: bi SI}
+Fixpoint use_tac_specialize_intuitionistic_helper `{SI: indexT} {M: bi}
     (Δ : envs M) (pats : list spec_pat) : bool :=
   match pats with
   | [] => false
diff --git a/theories/proofmode/modalities.v b/theories/proofmode/modalities.v
index 0f28f5f64087c24e6423fc0f29545c7a0b251402..ee01d3acfc724824c11f545ebbd5833ab78eb459 100644
--- a/theories/proofmode/modalities.v
+++ b/theories/proofmode/modalities.v
@@ -49,10 +49,10 @@ it is implemented as an endomapping. On the other hand, the embedding modality
 ⎡-⎤ is a mapping between propositions of different BI-algebras.
 *)
 
-Inductive modality_action {SI: indexT} (PROP1 : bi SI) : bi SI → Type :=
-  | MIEnvIsEmpty {PROP2 : bi SI} : modality_action PROP1 PROP2
+Inductive modality_action `{SI: indexT} (PROP1 : bi) : bi → Type :=
+  | MIEnvIsEmpty {PROP2 : bi} : modality_action PROP1 PROP2
   | MIEnvForall (C : PROP1 → Prop) : modality_action PROP1 PROP1
-  | MIEnvTransform {PROP2 : bi SI} (C : PROP2 → PROP1 → Prop) : modality_action PROP1 PROP2
+  | MIEnvTransform {PROP2 : bi} (C : PROP2 → PROP1 → Prop) : modality_action PROP1 PROP2
   | MIEnvClear {PROP2} : modality_action PROP1 PROP2
   | MIEnvId : modality_action PROP1 PROP1.
 Global Arguments MIEnvIsEmpty {_ _ _}.
@@ -63,7 +63,7 @@ Global Arguments MIEnvId {_ _}.
 
 Notation MIEnvFilter C := (MIEnvTransform (TCDiag C)).
 
-Definition modality_intuitionistic_action_spec {SI: indexT} {PROP1 PROP2: bi SI}
+Definition modality_intuitionistic_action_spec `{SI: indexT} {PROP1 PROP2: bi}
     (s : modality_action PROP1 PROP2) : (PROP1 → PROP2) → Prop :=
   match s with
   | MIEnvIsEmpty => λ M, True
@@ -77,7 +77,7 @@ Definition modality_intuitionistic_action_spec {SI: indexT} {PROP1 PROP2: bi SI}
   | MIEnvId => λ M, ∀ P, □ P ⊢ M (□ P)
   end.
 
-Definition modality_spatial_action_spec {SI} {PROP1 PROP2: bi SI}
+Definition modality_spatial_action_spec `{SI: indexT} {PROP1 PROP2: bi}
     (s : modality_action PROP1 PROP2) : (PROP1 → PROP2) → Prop :=
   match s with
   | MIEnvIsEmpty => λ M, True
@@ -89,7 +89,7 @@ Definition modality_spatial_action_spec {SI} {PROP1 PROP2: bi SI}
 
 (* A modality is then a record packing together the modality with the laws it
 should satisfy to justify the given actions for both contexts: *)
-Record modality_mixin {SI} {PROP1 PROP2 : bi SI} (M : PROP1 → PROP2)
+Record modality_mixin `{SI: indexT} {PROP1 PROP2 : bi} (M : PROP1 → PROP2)
     (iaction saction : modality_action PROP1 PROP2) := {
   modality_mixin_intuitionistic : modality_intuitionistic_action_spec iaction M;
   modality_mixin_spatial : modality_spatial_action_spec saction M;
@@ -98,7 +98,7 @@ Record modality_mixin {SI} {PROP1 PROP2 : bi SI} (M : PROP1 → PROP2)
   modality_mixin_sep P Q : M P ∗ M Q ⊢ M (P ∗ Q)
 }.
 
-Record modality {SI} (PROP1 PROP2 : bi SI) := Modality {
+Record modality `{SI: indexT} (PROP1 PROP2 : bi) := Modality {
   modality_car :> PROP1 → PROP2;
   modality_intuitionistic_action : modality_action PROP1 PROP2;
   modality_spatial_action : modality_action PROP1 PROP2;
@@ -110,7 +110,7 @@ Global Arguments modality_intuitionistic_action {_ _ _} _.
 Global Arguments modality_spatial_action {_ _ _} _.
 
 Section modality.
-  Context {SI: indexT} {PROP1 PROP2: bi SI} (M : modality PROP1 PROP2).
+  Context {SI: indexT} {PROP1 PROP2: bi} (M : modality PROP1 PROP2).
 
   Lemma modality_intuitionistic_transform C P Q :
     modality_intuitionistic_action M = MIEnvTransform C → C P Q → □ P ⊢ M (□ Q).
@@ -140,7 +140,7 @@ Section modality.
 End modality.
 
 Section modality1.
-  Context {SI: indexT} {PROP: bi SI} (M : modality PROP PROP).
+  Context {SI: indexT} {PROP: bi} (M : modality PROP PROP).
 
   Lemma modality_intuitionistic_forall C P :
     modality_intuitionistic_action M = MIEnvForall C → C P → □ P ⊢ M (□ P).
@@ -183,6 +183,6 @@ End modality1.
 which will instruct [iModIntro] to introduce the modality without modifying the
 proof mode context. Examples of such modalities are [bupd], [fupd], [except_0],
 [monPred_subjectively] and [bi_absorbingly]. *)
-Lemma modality_id_mixin {SI} {PROP : bi SI} : modality_mixin (@id PROP) MIEnvId MIEnvId.
+Lemma modality_id_mixin `{SI: indexT} {PROP : bi} : modality_mixin (@id PROP) MIEnvId MIEnvId.
 Proof. split; simpl; eauto. Qed.
-Definition modality_id {SI} {PROP : bi SI} := Modality (@id PROP) modality_id_mixin.
+Definition modality_id `{SI: indexT} {PROP : bi} := Modality (@id PROP) modality_id_mixin.
diff --git a/theories/proofmode/modality_instances.v b/theories/proofmode/modality_instances.v
index ae3e993dc20fed12f15d84849a451ae8be457046..97eb1fdcad7db9ad55583f22ef7d01b081b139dd 100644
--- a/theories/proofmode/modality_instances.v
+++ b/theories/proofmode/modality_instances.v
@@ -4,7 +4,7 @@ From iris.prelude Require Import options.
 Import bi.
 
 Section modalities.
-  Context {SI} {PROP : bi SI}.
+  Context `{SI: indexT} {PROP : bi}.
 
   Lemma modality_persistently_mixin :
     modality_mixin (@bi_persistently SI PROP) MIEnvId MIEnvClear.