diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index ed6ae154c6962b73faabf659e8b71b5442c76430..926f0ebe04e280e4e414af6f9c0be74560bdfe1d 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -12,9 +12,9 @@ agreement, i.e., [✓ (●{p1} a1 ⋅ ●{p2} a2) → a1 ≡ a2]. *)
 
 (** * Definition of the view relation *)
 (** The authoritative camera is obtained by instantiating the view camera. *)
-Definition auth_view_rel_raw {SI} {A : ucmra SI} (n : SI) (a b : A) : Prop :=
+Definition auth_view_rel_raw `{SI: indexT} {A : ucmra} (n : index) (a b : A) : Prop :=
   b ≼{n} a ∧ ✓{n} a.
-Lemma auth_view_rel_raw_mono {SI} (A : ucmra SI) n1 n2 (a1 a2 b1 b2 : A) :
+Lemma auth_view_rel_raw_mono `{SI: indexT} (A : ucmra) n1 n2 (a1 a2 b1 b2 : A) :
   auth_view_rel_raw n1 a1 b1 →
   a1 ≡{n2}≡ a2 →
   b2 ≼{n2} b1 →
@@ -25,26 +25,26 @@ Proof.
   - trans b1; [done|]. rewrite -Ha12. by apply cmra_includedN_le with n1.
   - rewrite -Ha12. by apply cmra_validN_le with n1.
 Qed.
-Lemma auth_view_rel_raw_valid {SI} (A : ucmra SI) n (a b : A) :
+Lemma auth_view_rel_raw_valid `{SI: indexT} (A : ucmra) n (a b : A) :
   auth_view_rel_raw n a b → ✓{n} b.
 Proof. intros [??]; eauto using cmra_validN_includedN. Qed.
-Lemma auth_view_rel_raw_unit {SI} (A : ucmra SI) n :
+Lemma auth_view_rel_raw_unit `{SI: indexT} (A : ucmra) n :
   ∃ a : A, auth_view_rel_raw n a ε.
 Proof. exists ε. split; [done|]. apply ucmra_unit_validN. Qed.
-Canonical Structure auth_view_rel {SI} {A : ucmra SI} : view_rel A A :=
+Canonical Structure auth_view_rel `{SI: indexT} {A : ucmra} : view_rel A A :=
   ViewRel auth_view_rel_raw (auth_view_rel_raw_mono A)
           (auth_view_rel_raw_valid A) (auth_view_rel_raw_unit A).
 
-Lemma auth_view_rel_unit {SI} {A : ucmra SI} n (a : A) : auth_view_rel n a ε ↔ ✓{n} a.
+Lemma auth_view_rel_unit `{SI: indexT} {A : ucmra} n (a : A) : auth_view_rel n a ε ↔ ✓{n} a.
 Proof. split; [by intros [??]|]. split; auto using ucmra_unit_leastN. Qed.
-Lemma auth_view_rel_exists {SI} {A : ucmra SI} n (b : A) :
+Lemma auth_view_rel_exists `{SI: indexT} {A : ucmra} n (b : A) :
   (∃ a, auth_view_rel n a b) ↔ ✓{n} b.
 Proof.
   split; [|intros; exists b; by split].
   intros [a Hrel]. eapply auth_view_rel_raw_valid, Hrel.
 Qed.
 
-Global Instance auth_view_rel_discrete {SI} {A : ucmra SI} :
+Global Instance auth_view_rel_discrete `{SI: indexT} {A : ucmra} :
   CmraDiscrete A → ViewRelDiscrete (auth_view_rel (A:=A)).
 Proof.
   intros ? n a b [??]; split.
@@ -57,14 +57,14 @@ Qed.
 This way, one can use [auth A] with [A : Type] instead of [A : ucmra], and let
 canonical structure search determine the corresponding camera instance. *)
 Notation auth A := (view (A:=A) (B:=A) auth_view_rel_raw).
-Definition authO {SI} (A : ucmra SI) : ofe SI := viewO (A:=A) (B:=A) auth_view_rel.
-Definition authR {SI} (A : ucmra SI) : cmra SI := viewR (A:=A) (B:=A) auth_view_rel.
-Definition authUR {SI} (A : ucmra SI) : ucmra SI := viewUR (A:=A) (B:=A) auth_view_rel.
+Definition authO `{SI: indexT} (A : ucmra) : ofe := viewO (A:=A) (B:=A) auth_view_rel.
+Definition authR `{SI: indexT} (A : ucmra) : cmra := viewR (A:=A) (B:=A) auth_view_rel.
+Definition authUR `{SI: indexT} (A : ucmra) : ucmra := viewUR (A:=A) (B:=A) auth_view_rel.
 
-Definition auth_auth {SI} {A: ucmra SI} : Qp → A → auth A := view_auth.
-Definition auth_frag {SI} {A: ucmra SI} : A → auth A := view_frag.
+Definition auth_auth `{SI: indexT} {A: ucmra} : Qp → A → auth A := view_auth.
+Definition auth_frag `{SI: indexT} {A: ucmra} : A → auth A := view_frag.
 
-Typeclasses Opaque auth_auth auth_frag.
+Global Typeclasses Opaque auth_auth auth_frag.
 
 Global Instance: Params (@auth_frag) 2 := {}.
 Global Instance: Params (@auth_auth) 2 := {}.
@@ -78,7 +78,7 @@ Notation "● a" := (auth_auth 1 a) (at level 20).
 general version in terms of [●] and [◯], and because such a lemma has never
 been needed in practice. *)
 Section auth.
-  Context {SI} {A : ucmra SI}.
+  Context `{SI: indexT} {A : ucmra}.
   Implicit Types a b : A.
   Implicit Types x y : auth A.
 
@@ -114,7 +114,7 @@ Section auth.
   Lemma auth_auth_frac_op p q a : ●{p + q} a ≡ ●{p} a ⋅ ●{q} a.
   Proof. apply view_auth_frac_op. Qed.
   Global Instance auth_auth_frac_is_op q q1 q2 a :
-    IsOp (q: fracO SI) q1 q2 → IsOp' (●{q} a) (●{q1} a) (●{q2} a).
+    IsOp q q1 q2 → IsOp' (●{q} a) (●{q1} a) (●{q2} a).
   Proof. rewrite /auth_auth. apply _. Qed.
 
   Lemma auth_frag_op a b : ◯ (a ⋅ b) = ◯ a ⋅ ◯ b.
@@ -333,7 +333,7 @@ Section auth.
 End auth.
 
 (** * Functor *)
-Program Definition authURF {SI} (F : urFunctor SI) : urFunctor SI := {|
+Program Definition authURF `{SI: indexT} (F : urFunctor) : urFunctor := {|
   urFunctor_car A B := authUR (urFunctor_car F A B);
   urFunctor_map A1 A2 B1 B2 fg :=
     viewO_map (urFunctor_map F fg) (urFunctor_map F fg)
@@ -358,27 +358,20 @@ Next Obligation.
   - by apply (cmra_morphism_validN _).
 Qed.
 
-Global Instance authURF_contractive {SI} (F : urFunctor SI):
+Global Instance authURF_contractive `{SI: indexT} (F : urFunctor):
   urFunctorContractive F → urFunctorContractive (authURF F).
 Proof.
   intros ? A1 A2 B1 B2 n f g Hfg.
   apply viewO_map_ne; by apply urFunctor_map_contractive.
 Qed.
 
-Program Definition authRF {SI} (F : urFunctor SI) : rFunctor SI := {|
+Program Definition authRF `{SI: indexT} (F : urFunctor) : rFunctor := {|
   rFunctor_car A B := authR (urFunctor_car F A B);
   rFunctor_map A1 A2 B1 B2 fg :=
     viewO_map (urFunctor_map F fg) (urFunctor_map F fg)
 |}.
-(* TODO: fix this proof *)
-Next Obligation. intros; apply authURF. Qed.
-Next Obligation. intros; apply authURF. Qed.
-Next Obligation.
-  intros; simpl. rewrite -view_map_compose.
-  apply (view_map_ext _ _ _ _)=> y; apply urFunctor_map_compose.
-Qed.
-Next Obligation. intros; apply authURF. Qed.
+Solve Obligations with (intros SI; intros; apply (@authURF SI)).
 
-Global Instance authRF_contractive {SI} (F : urFunctor SI):
+Global Instance authRF_contractive `{SI: indexT} (F : urFunctor):
   urFunctorContractive F → rFunctorContractive (authRF F).
 Proof. apply authURF_contractive. Qed.
diff --git a/theories/algebra/coPset.v b/theories/algebra/coPset.v
index 51212edeca43773ca0b7ea19b4afbe7eaf5fb19a..03dd9a77d2f8bb2b5cd722562f17487db3cb104b 100644
--- a/theories/algebra/coPset.v
+++ b/theories/algebra/coPset.v
@@ -7,10 +7,10 @@ generalize the construction without breaking canonical structures. *)
 
 (* The union CMRA *)
 Section coPset.
-  Context {SI: indexT}.
+  Context `{SI: indexT}.
   Implicit Types X Y : coPset.
 
-  Canonical Structure coPsetO := discreteO SI coPset.
+  Canonical Structure coPsetO := discreteO coPset.
 
   Local Instance coPset_valid_instance : Valid coPset := λ _, True.
   Local Instance coPset_unit_instance : Unit coPset := (∅ : coPset).
@@ -38,14 +38,14 @@ Section coPset.
     - intros X1 X2. by rewrite !coPset_op_union comm_L.
     - intros X. by rewrite coPset_core_self idemp_L.
   Qed.
-  Canonical Structure coPsetR := discreteR SI coPset coPset_ra_mixin.
+  Canonical Structure coPsetR := discreteR coPset coPset_ra_mixin.
 
   Global Instance coPset_cmra_discrete : CmraDiscrete coPsetR.
   Proof. apply discrete_cmra_discrete. Qed.
 
-  Lemma coPset_ucmra_mixin : UcmraMixin SI coPset.
+  Lemma coPset_ucmra_mixin : UcmraMixin coPset.
   Proof. split; [done | | done]. intros X. by rewrite coPset_op_union left_id_L. Qed.
-  Canonical Structure coPsetUR := Ucmra SI coPset coPset_ucmra_mixin.
+  Canonical Structure coPsetUR := Ucmra coPset coPset_ucmra_mixin.
 
   Lemma coPset_opM X mY : X ⋅? mY = X ∪ default ∅ mY.
   Proof. destruct mY; by rewrite /= ?right_id_L. Qed.
@@ -60,9 +60,6 @@ Section coPset.
     split; first done. rewrite coPset_op_union. set_solver.
   Qed.
 End coPset.
-Arguments coPsetO : clear implicits.
-Arguments coPsetR : clear implicits.
-Arguments coPsetUR : clear implicits.
 
 (* The disjoiny union CMRA *)
 Inductive coPset_disj :=
@@ -72,9 +69,9 @@ Global Instance inhabited_coPset_disj: Inhabited (coPset_disj).
 Proof. split; by constructor 2. Qed.
 
 Section coPset_disj.
-  Context {SI: indexT}.
+  Context `{SI: indexT}.
   Local Arguments op _ _ !_ !_ /.
-  Canonical Structure coPset_disjO := leibnizO SI coPset_disj.
+  Canonical Structure coPset_disjO := leibnizO coPset_disj.
 
   Local Instance coPset_disj_valid_instance : Valid coPset_disj := λ X,
     match X with CoPset _ => True | CoPsetBot => False end.
@@ -117,16 +114,12 @@ Section coPset_disj.
     - exists (CoPset ∅); coPset_disj_solve.
     - intros [X1|] [X2|]; coPset_disj_solve.
   Qed.
-  Canonical Structure coPset_disjR := discreteR SI coPset_disj coPset_disj_ra_mixin.
+  Canonical Structure coPset_disjR := discreteR coPset_disj coPset_disj_ra_mixin.
 
   Global Instance coPset_disj_cmra_discrete : CmraDiscrete coPset_disjR.
   Proof. apply discrete_cmra_discrete. Qed.
 
-  Lemma coPset_disj_ucmra_mixin : UcmraMixin SI coPset_disj.
+  Lemma coPset_disj_ucmra_mixin : UcmraMixin coPset_disj.
   Proof. split; try apply _ || done. intros [X|]; coPset_disj_solve. Qed.
-  Canonical Structure coPset_disjUR := Ucmra SI coPset_disj coPset_disj_ucmra_mixin.
+  Canonical Structure coPset_disjUR := Ucmra coPset_disj coPset_disj_ucmra_mixin.
 End coPset_disj.
-
-Arguments coPset_disjO : clear implicits.
-Arguments coPset_disjR : clear implicits.
-Arguments coPset_disjUR : clear implicits.
\ No newline at end of file
diff --git a/theories/algebra/csum.v b/theories/algebra/csum.v
index 0d5b338309117f55da6031fbdf49bc1f9ece2a28..6ebaa962df99f51e0343a3af0145e803965af2e5 100644
--- a/theories/algebra/csum.v
+++ b/theories/algebra/csum.v
@@ -27,7 +27,7 @@ Global Instance maybe_Cinr {A B} : Maybe (@Cinr A B) := λ x,
   match x with Cinr b => Some b | _ => None end.
 
 Section ofe.
-Context {SI : indexT} {A B : ofe SI}.
+Context `{SI : indexT} {A B : ofe}.
 Implicit Types a : A.
 Implicit Types b : B.
 
@@ -37,7 +37,7 @@ Inductive csum_equiv : Equiv (csum A B) :=
   | Cinr_equiv b b' : b ≡ b' → Cinr b ≡ Cinr b'
   | CsumBot_equiv : CsumBot ≡ CsumBot.
 Existing Instance csum_equiv.
-Inductive csum_dist : Dist SI (csum A B) :=
+Inductive csum_dist : Dist (csum A B) :=
   | Cinl_dist n a a' : a ≡{n}≡ a' → Cinl a ≡{n}≡ Cinl a'
   | Cinr_dist n b b' : b ≡{n}≡ b' → Cinr b ≡{n}≡ Cinr b'
   | CsumBot_dist n : CsumBot ≡{n}≡ CsumBot.
@@ -60,7 +60,7 @@ Proof. by inversion_clear 1. Qed.
 Global Instance Cinr_inj_dist n : Inj (dist n) (dist n) (@Cinr A B).
 Proof. by inversion_clear 1. Qed.
 
-Definition csum_ofe_mixin : OfeMixin SI (csum A B).
+Definition csum_ofe_mixin : OfeMixin (csum A B).
 Proof.
   split.
   - intros mx my; split.
@@ -73,7 +73,7 @@ Proof.
     + destruct 1; inversion_clear 1; constructor; etrans; eauto.
   - inversion_clear 1; constructor; by eapply dist_mono.
 Qed.
-Canonical Structure csumO : ofe SI := Ofe (csum A B) csum_ofe_mixin.
+Canonical Structure csumO : ofe := Ofe (csum A B) csum_ofe_mixin.
 
 Program Definition csum_chain_l (c : chain csumO) (a : A) : chain A :=
   {| chain_car n := match c n return _ with Cinl a' => a' | _ => a end |}.
@@ -93,14 +93,14 @@ Next Obligation. intros α c a β γ Hle Hβ Hγ. cbn. by destruct (bchain_cauch
 Program Definition csum_bchain_r {α} (c : bchain csumO α) (b : B) : bchain B α :=
   {| bchain_car β Hβ := match c β Hβ return _ with Cinr b' => b' | _ => b end |}.
 Next Obligation. intros α c b β γ Hle Hβ Hγ. cbn. by destruct (bchain_cauchy _ c β γ Hle Hβ Hγ). Qed.
-Definition csum_lbcompl {HA:Cofe A} {HB: Cofe B} (α : SI):= λ (Hl : index_is_proper_limit α) (c : bchain csumO α),
+Definition csum_lbcompl {HA: Cofe A} {HB: Cofe B} (α : index):= λ (Hl : index_is_proper_limit α) (c : bchain csumO α),
   match c zero (proper_limit_not_zero Hl) with
   | Cinl a => Cinl (lbcompl Hl (csum_bchain_l c a))
   | Cinr b => Cinr (lbcompl Hl (csum_bchain_r c b))
   | CsumBot => CsumBot
   end.
 
-Global Program Instance csum_cofe `{Cofe SI A, Cofe SI B} : Cofe csumO :=
+Global Program Instance csum_cofe `{!Cofe A, !Cofe B} : Cofe csumO :=
   {| compl := csum_compl; lbcompl := csum_lbcompl |}.
 Next Obligation.
   intros ?? α c; rewrite /compl /csum_compl.
@@ -135,7 +135,7 @@ Proof. by inversion_clear 2; constructor; apply (discrete _). Qed.
 
 End ofe.
 
-Global Arguments csumO : clear implicits.
+Global Arguments csumO {_} _ _.
 
 (* Functor on COFEs *)
 Definition csum_map {A A' B B'} (fA : A → A') (fB : B → B')
@@ -153,22 +153,22 @@ Lemma csum_map_compose {A A' A'' B B' B''} (f : A → A') (f' : A' → A'')
                        (g : B → B') (g' : B' → B'') (x : csum A B) :
   csum_map (f' ∘ f) (g' ∘ g) x = csum_map f' g' (csum_map f g x).
 Proof. by destruct x. Qed.
-Lemma csum_map_ext {SI} {A A' B B' : ofe SI} (f f' : A → A') (g g' : B → B') x :
+Lemma csum_map_ext `{SI: indexT} {A A' B B' : ofe} (f f' : A → A') (g g' : B → B') x :
   (∀ x, f x ≡ f' x) → (∀ x, g x ≡ g' x) → csum_map f g x ≡ csum_map f' g' x.
 Proof. by destruct x; constructor. Qed.
-Global Instance csum_map_cmra_ne {SI} {A A' B B' : ofe SI} n :
+Global Instance csum_map_cmra_ne `{SI: indexT} {A A' B B' : ofe} n :
   Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==> dist n ==> dist n)
          (@csum_map A A' B B').
 Proof. intros f f' Hf g g' Hg []; destruct 1; constructor; by apply Hf || apply Hg. Qed.
-Definition csumO_map {SI} {A A' B B'} (f : A -n> A') (g : B -n> B') :
-  csumO SI A B -n> csumO SI A' B' :=
+Definition csumO_map `{SI: indexT} {A A' B B'} (f : A -n> A') (g : B -n> B') :
+  csumO A B -n> csumO A' B' :=
   OfeMor (csum_map f g).
-Global Instance csumO_map_ne {SI} {A A' B B' : ofe SI} :
+Global Instance csumO_map_ne `{SI: indexT} {A A' B B' : ofe} :
   NonExpansive2 (@csumO_map SI A A' B B').
 Proof. by intros n f f' Hf g g' Hg []; constructor. Qed.
 
 Section cmra.
-Context {SI : indexT} {A B : cmra SI}.
+Context `{SI: indexT} {A B : cmra}.
 Implicit Types a : A.
 Implicit Types b : B.
 
@@ -179,7 +179,7 @@ Local Instance csum_valid_instance : Valid (csum A B) := λ x,
   | Cinr b => ✓ b
   | CsumBot => False
   end.
-Local Instance csum_validN_instance : ValidN SI (csum A B) := λ n x,
+Local Instance csum_validN_instance : ValidN (csum A B) := λ n x,
   match x with
   | Cinl a => ✓{n} a
   | Cinr b => ✓{n} b
@@ -243,7 +243,7 @@ Proof.
     + exists (Cinr c); by constructor.
 Qed.
 
-Lemma csum_cmra_mixin : CmraMixin SI (csum A B).
+Lemma csum_cmra_mixin : CmraMixin (csum A B).
 Proof.
   split.
   - intros [] n; destruct 1; constructor; by ofe_subst.
@@ -288,7 +288,7 @@ Proof.
       exists (Cinr z1), (Cinr z2). by repeat constructor.
     + by exists CsumBot, CsumBot; destruct y1, y2; inversion_clear Hx'.
 Qed.
-Canonical Structure csumR := Cmra SI (csum A B) csum_cmra_mixin.
+Canonical Structure csumR := Cmra (csum A B) csum_cmra_mixin.
 
 Global Instance csum_cmra_discrete :
   CmraDiscrete A → CmraDiscrete B → CmraDiscrete csumR.
@@ -397,10 +397,10 @@ Proof.
 Qed.
 End cmra.
 
-Global Arguments csumR : clear implicits.
+Global Arguments csumR {_} _ _.
 
 (* Functor *)
-Global Instance csum_map_cmra_morphism {SI} {A A' B B' : cmra SI} (f : A → A') (g : B → B') :
+Global Instance csum_map_cmra_morphism `{SI: indexT} {A A' B B' : cmra} (f : A → A') (g : B → B') :
   CmraMorphism f → CmraMorphism g → CmraMorphism (csum_map f g).
 Proof.
   split; try apply _.
@@ -411,8 +411,8 @@ Proof.
   - intros [xa|ya|] [xb|yb|]=>//=; by rewrite cmra_morphism_op.
 Qed.
 
-Program Definition csumRF {SI} (Fa Fb : rFunctor SI) : rFunctor SI := {|
-  rFunctor_car A B := csumR SI (rFunctor_car Fa A B) (rFunctor_car Fb A B);
+Program Definition csumRF `{SI: indexT} (Fa Fb : rFunctor) : rFunctor := {|
+  rFunctor_car A B := csumR (rFunctor_car Fa A B) (rFunctor_car Fb A B);
   rFunctor_map A1 A2 B1 B2 fg := csumO_map (rFunctor_map Fa fg) (rFunctor_map Fb fg)
 |}.
 Next Obligation.
@@ -427,7 +427,7 @@ Next Obligation.
   apply csum_map_ext=>y; apply rFunctor_map_compose.
 Qed.
 
-Global Instance csumRF_contractive {SI} (Fa Fb : rFunctor SI) :
+Global Instance csumRF_contractive `{SI: indexT} (Fa Fb : rFunctor) :
   rFunctorContractive Fa → rFunctorContractive Fb →
   rFunctorContractive (csumRF Fa Fb).
 Proof.
diff --git a/theories/algebra/dfrac.v b/theories/algebra/dfrac.v
index 4227746f634534c298213a0a3d3ae18dbd0b6e62..57c0f086deff98c24f222ed82289bbb88864faf3 100644
--- a/theories/algebra/dfrac.v
+++ b/theories/algebra/dfrac.v
@@ -33,8 +33,8 @@ Inductive dfrac :=
   | DfracBoth : Qp → dfrac.
 
 Section dfrac.
-  Context {SI: indexT}.
-  Canonical Structure dfracO := leibnizO SI dfrac.
+  Context `{SI: indexT}.
+  Canonical Structure dfracO := leibnizO dfrac.
 
   Implicit Types p q : Qp.
   Implicit Types dp dq : dfrac.
@@ -134,7 +134,7 @@ Section dfrac.
       + intros. trans (q + q')%Qp; [|done]. apply Qp.lt_add_l.
       + intros. trans (q + q')%Qp; [|done]. apply Qp.lt_add_l.
   Qed.
-  Canonical Structure dfracR := discreteR SI dfrac dfrac_ra_mixin.
+  Canonical Structure dfracR := discreteR dfrac dfrac_ra_mixin.
 
   Global Instance dfrac_cmra_discrete : CmraDiscrete dfracR.
   Proof. apply discrete_cmra_discrete. Qed.
@@ -169,8 +169,8 @@ Section dfrac.
     - intro Hlt. etrans; last apply Hlt. apply Qp.lt_add_r.
   Qed.
 
-  Lemma dfrac_valid_own_l dq q: ✓ (DfracOwn (q : fracO SI) ⋅ dq) → (q < 1)%Qp.
-  Proof. rewrite comm. apply dfrac_valid_own_r. Qed.
+  Lemma dfrac_valid_own_l dq q: ✓ (DfracOwn q ⋅ dq) → (q < 1)%Qp.
+  Proof using SI. rewrite comm. apply dfrac_valid_own_r. Qed.
 
   Lemma dfrac_valid_discarded p : ✓ DfracDiscarded.
   Proof. done. Qed.
@@ -180,7 +180,7 @@ Section dfrac.
   Proof. done. Qed.
 
   Global Instance dfrac_is_op q q1 q2 :
-    IsOp (q: fracO SI) q1 q2 →
+    IsOp q q1 q2 →
     IsOp' (DfracOwn q) (DfracOwn q1) (DfracOwn q2).
   Proof. rewrite /IsOp' /IsOp dfrac_op_own=>-> //. Qed.
 
@@ -193,5 +193,3 @@ Section dfrac.
   Qed.
 
 End dfrac.
-Arguments dfracO : clear implicits.
-Arguments dfracR : clear implicits.
diff --git a/theories/algebra/functions.v b/theories/algebra/functions.v
index ebc3f59794e476d4b3a94e0d8f8ae651f81ad5d6..4484fdc11613ba8b0b69de98e6c676a032b84645 100644
--- a/theories/algebra/functions.v
+++ b/theories/algebra/functions.v
@@ -3,17 +3,17 @@ From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates.
 From iris.prelude Require Import options.
 
-Definition discrete_fun_insert `{EqDecision A} {SI} {B : A → ofe SI}
+Definition discrete_fun_insert `{EqDecision A} `{SI: indexT} {B : A → ofe}
     (x : A) (y : B x) (f : discrete_fun B) : discrete_fun B := λ x',
   match decide (x = x') with left H => eq_rect _ B y _ H | right _ => f x' end.
 Global Instance: Params (@discrete_fun_insert) 6 := {}.
 
-Definition discrete_fun_singleton `{EqDecision A} {SI} {B : A → ucmra SI}
+Definition discrete_fun_singleton `{EqDecision A} `{SI: indexT} {B : A → ucmra}
   (x : A) (y : B x) : discrete_fun B := discrete_fun_insert x y ε.
 Global Instance: Params (@discrete_fun_singleton) 6 := {}.
 
 Section ofe.
-  Context `{Heqdec : EqDecision A} {SI} {B : A → ofe SI}.
+  Context `{Heqdec : EqDecision A} `{SI: indexT} {B : A → ofe}.
   Implicit Types x : A.
   Implicit Types f g : discrete_fun B.
 
@@ -52,7 +52,7 @@ Section ofe.
 End ofe.
 
 Section cmra.
-  Context `{EqDecision A} {SI} {B : A → ucmra SI}.
+  Context `{EqDecision A} `{SI: indexT} {B : A → ucmra}.
   Implicit Types x : A.
   Implicit Types f g : discrete_fun B.
 
diff --git a/theories/algebra/gmultiset.v b/theories/algebra/gmultiset.v
index 5255045c6e38582a33c93b08ee0064fe9edc8413..aa93316456e73ff761b948cc11af87c03755b424 100644
--- a/theories/algebra/gmultiset.v
+++ b/theories/algebra/gmultiset.v
@@ -5,13 +5,13 @@ From iris.prelude Require Import options.
 
 (* The multiset union CMRA *)
 Section gmultiset.
-  Context {SI : indexT} `{Countable K}.
+  Context `{SI : indexT} `{Countable K}.
   Implicit Types X Y : gmultiset K.
 
-  Canonical Structure gmultisetO := discreteO SI (gmultiset K).
+  Canonical Structure gmultisetO := discreteO (gmultiset K).
 
   Local Instance gmultiset_valid_instance : Valid (gmultiset K) := λ _, True.
-  Local Instance gmultiset_validN_instance : ValidN SI (gmultiset K) := λ _ _, True.
+  Local Instance gmultiset_validN_instance : ValidN (gmultiset K) := λ _ _, True.
   Local Instance gmultiset_unit_instance : Unit (gmultiset K) := (∅ : gmultiset K).
   Local Instance gmultiset_op_instance : Op (gmultiset K) := disj_union.
   Local Instance gmultiset_pcore_instance : PCore (gmultiset K) := λ X, Some ∅.
@@ -41,17 +41,17 @@ Section gmultiset.
       by rewrite left_id.
   Qed.
 
-  Canonical Structure gmultisetR := discreteR SI (gmultiset K) gmultiset_ra_mixin.
+  Canonical Structure gmultisetR := discreteR (gmultiset K) gmultiset_ra_mixin.
 
   Global Instance gmultiset_cmra_discrete : CmraDiscrete gmultisetR.
   Proof. apply discrete_cmra_discrete. Qed.
 
-  Lemma gmultiset_ucmra_mixin : UcmraMixin SI (gmultiset K).
+  Lemma gmultiset_ucmra_mixin : UcmraMixin (gmultiset K).
   Proof.
     split; [done | | done]. intros X.
     by rewrite gmultiset_op_disj_union left_id_L.
   Qed.
-  Canonical Structure gmultisetUR := Ucmra SI (gmultiset K) gmultiset_ucmra_mixin.
+  Canonical Structure gmultisetUR := Ucmra (gmultiset K) gmultiset_ucmra_mixin.
 
   Global Instance gmultiset_cancelable X : Cancelable X.
   Proof.
@@ -95,6 +95,6 @@ Section gmultiset.
 
 End gmultiset.
 
-Global Arguments gmultisetO _ _ {_ _}.
-Global Arguments gmultisetR _ _ {_ _}.
-Global Arguments gmultisetUR _ _ {_ _}.
+Global Arguments gmultisetO {_} _ {_ _}.
+Global Arguments gmultisetR {_} _ {_ _}.
+Global Arguments gmultisetUR {_} _ {_ _}.
diff --git a/theories/algebra/gset.v b/theories/algebra/gset.v
index 8780eddbe476d09bade1d6166c577df00fa29071..97dda0b1c20e60ed08b95921836eb2717317057d 100644
--- a/theories/algebra/gset.v
+++ b/theories/algebra/gset.v
@@ -5,10 +5,10 @@ From iris.prelude Require Import options.
 
 (* The union CMRA *)
 Section gset.
-  Context {SI: indexT} `{Countable K}.
+  Context `{SI: indexT} `{Countable K}.
   Implicit Types X Y : gset K.
 
-  Canonical Structure gsetO := discreteO SI (gset K).
+  Canonical Structure gsetO := discreteO (gset K).
 
   Local Instance gset_valid_instance : Valid (gset K) := λ _, True.
   Local Instance gset_unit_instance : Unit (gset K) := (∅ : gset K).
@@ -31,14 +31,14 @@ Section gset.
     apply ra_total_mixin; apply _ || eauto; [].
     intros X. by rewrite gset_core_self idemp_L.
   Qed.
-  Canonical Structure gsetR := discreteR SI (gset K) gset_ra_mixin.
+  Canonical Structure gsetR := discreteR (gset K) gset_ra_mixin.
 
   Global Instance gset_cmra_discrete : CmraDiscrete gsetR.
   Proof. apply discrete_cmra_discrete. Qed.
 
-  Lemma gset_ucmra_mixin : UcmraMixin SI (gset K).
+  Lemma gset_ucmra_mixin : UcmraMixin (gset K).
   Proof. split; [ done | | done ]. intros X. by rewrite gset_op_union left_id_L. Qed.
-  Canonical Structure gsetUR := Ucmra SI (gset K) gset_ucmra_mixin.
+  Canonical Structure gsetUR := Ucmra (gset K) gset_ucmra_mixin.
 
   Lemma gset_opM X mY : X ⋅? mY = X ∪ default ∅ mY.
   Proof. destruct mY; by rewrite /= ?right_id_L. Qed.
@@ -81,12 +81,12 @@ Global Instance gset_disj_inhab K `{Countable K}: Inhabited (gset_disj K).
 Proof. constructor. exact GSetBot. Qed.
 
 Section gset_disj.
-  Context {SI: indexT} `{Countable K}.
+  Context `{SI: indexT} `{Countable K}.
   Local Arguments op _ _ !_ !_ /.
   Local Arguments cmra_op _ !_ !_ /.
   Local Arguments ucmra_op _ !_ !_ /.
 
-  Canonical Structure gset_disjO := leibnizO SI (gset_disj K).
+  Canonical Structure gset_disjO := leibnizO (gset_disj K).
 
   Local Instance gset_disj_valid_instance : Valid (gset_disj K) := λ X,
     match X with GSet _ => True | GSetBot => False end.
@@ -128,14 +128,14 @@ Section gset_disj.
     - exists (GSet ∅); gset_disj_solve.
     - intros [X1|] [X2|]; gset_disj_solve.
   Qed.
-  Canonical Structure gset_disjR := discreteR SI (gset_disj K) gset_disj_ra_mixin.
+  Canonical Structure gset_disjR := discreteR (gset_disj K) gset_disj_ra_mixin.
 
   Global Instance gset_disj_cmra_discrete : CmraDiscrete gset_disjR.
   Proof. apply discrete_cmra_discrete. Qed.
 
-  Lemma gset_disj_ucmra_mixin : UcmraMixin SI (gset_disj K).
+  Lemma gset_disj_ucmra_mixin : UcmraMixin (gset_disj K).
   Proof. split; try apply _ || done. intros [X|]; gset_disj_solve. Qed.
-  Canonical Structure gset_disjUR := Ucmra SI (gset_disj K) gset_disj_ucmra_mixin.
+  Canonical Structure gset_disjUR := Ucmra (gset_disj K) gset_disj_ucmra_mixin.
 
   Local Arguments op _ _ _ _ : simpl never.
 
diff --git a/theories/algebra/lib/excl_auth.v b/theories/algebra/lib/excl_auth.v
index b8a0701b6d6aa6be49bb7b2fc077e6b03a8e59b5..55b2ffdc17aa6a9134ede03568a54f4660470a88 100644
--- a/theories/algebra/lib/excl_auth.v
+++ b/theories/algebra/lib/excl_auth.v
@@ -6,17 +6,17 @@ From iris.prelude Require Import options.
 This is effectively a single "ghost variable" with two views, the frament [◯E a]
 and the authority [●E a]. *)
 
-Definition excl_authR {SI} (A : ofe SI) : cmra SI :=
+Definition excl_authR `{SI: indexT} (A : ofe) : cmra :=
   authR (optionUR (exclR A)).
-Definition excl_authUR {SI} (A : ofe SI) : ucmra SI :=
+Definition excl_authUR `{SI: indexT} (A : ofe) : ucmra :=
   authUR (optionUR (exclR A)).
 
-Definition excl_auth_auth {SI} {A : ofe SI} (a : A) : excl_authR A :=
+Definition excl_auth_auth `{SI: indexT} {A : ofe} (a : A) : excl_authR A :=
   ● (Some (Excl a)).
-Definition excl_auth_frag {SI} {A : ofe SI} (a : A) : excl_authR A :=
+Definition excl_auth_frag `{SI: indexT} {A : ofe} (a : A) : excl_authR A :=
   ◯ (Some (Excl a)).
 
-Typeclasses Opaque excl_auth_auth excl_auth_frag.
+Global Typeclasses Opaque excl_auth_auth excl_auth_frag.
 
 Global Instance: Params (@excl_auth_auth) 2 := {}.
 Global Instance: Params (@excl_auth_frag) 3 := {}.
@@ -25,7 +25,7 @@ Notation "●E a" := (excl_auth_auth a) (at level 10).
 Notation "◯E a" := (excl_auth_frag a) (at level 10).
 
 Section excl_auth.
-  Context {SI} {A : ofe SI}.
+  Context `{SI: indexT} {A : ofe}.
   Implicit Types a b : A.
 
   Global Instance excl_auth_auth_ne : NonExpansive (@excl_auth_auth SI A).
diff --git a/theories/algebra/lib/frac_agree.v b/theories/algebra/lib/frac_agree.v
index 39862cbfc28d3476f8af9f8787a1d7a55613eadc..2fb680377fa645277859865169135285ef189f19 100644
--- a/theories/algebra/lib/frac_agree.v
+++ b/theories/algebra/lib/frac_agree.v
@@ -2,13 +2,13 @@ From iris.algebra Require Export frac agree updates local_updates.
 From iris.algebra Require Import proofmode_classes.
 From iris.prelude Require Import options.
 
-Definition frac_agreeR {SI} (A : ofe SI) : cmra SI := prodR (fracR SI) (agreeR A).
+Definition frac_agreeR `{SI: indexT} (A : ofe) : cmra := prodR fracR (agreeR A).
 
-Definition to_frac_agree {SI} {A : ofe SI} (q : frac) (a : A) : frac_agreeR A :=
+Definition to_frac_agree `{SI: indexT} {A : ofe} (q : frac) (a : A) : frac_agreeR A :=
   (q, to_agree a).
 
 Section lemmas.
-  Context {SI} {A : ofe SI}.
+  Context `{SI: indexT} {A : ofe}.
   Implicit Types (q : frac) (a : A).
 
   Global Instance to_frac_agree_ne q : NonExpansive (@to_frac_agree SI A q).
@@ -53,4 +53,4 @@ Section lemmas.
 
 End lemmas.
 
-Typeclasses Opaque to_frac_agree.
+Global Typeclasses Opaque to_frac_agree.
diff --git a/theories/algebra/lib/frac_auth.v b/theories/algebra/lib/frac_auth.v
index 4080a7173c796ec11a633794ce8c7e428393dabd..337e753ac696db33616963926cdba14c015a0248 100644
--- a/theories/algebra/lib/frac_auth.v
+++ b/theories/algebra/lib/frac_auth.v
@@ -9,17 +9,17 @@ From iris.prelude Require Import options.
   split the authoritative part into fractions.
 *)
 
-Definition frac_authR {SI} (A : cmra SI) : cmra SI :=
-  authR (optionUR (prodR (fracR SI) A)).
-Definition frac_authUR {SI} (A : cmra SI) : ucmra SI :=
-  authUR (optionUR (prodR (fracR SI) A)).
+Definition frac_authR `{SI: indexT} (A : cmra) : cmra :=
+  authR (optionUR (prodR fracR A)).
+Definition frac_authUR `{SI: indexT} (A : cmra) : ucmra :=
+  authUR (optionUR (prodR fracR A)).
 
-Definition frac_auth_auth {SI} {A : cmra SI} (x : A) : frac_authR A :=
+Definition frac_auth_auth `{SI: indexT} {A : cmra} (x : A) : frac_authR A :=
   ● (Some (1%Qp,x)).
-Definition frac_auth_frag {SI} {A : cmra SI} (q : frac) (x : A) : frac_authR A :=
+Definition frac_auth_frag `{SI: indexT} {A : cmra} (q : frac) (x : A) : frac_authR A :=
   ◯ (Some (q,x)).
 
-Typeclasses Opaque frac_auth_auth frac_auth_frag.
+Global Typeclasses Opaque frac_auth_auth frac_auth_frag.
 
 Global Instance: Params (@frac_auth_auth) 2 := {}.
 Global Instance: Params (@frac_auth_frag) 3 := {}.
@@ -29,7 +29,7 @@ Notation "◯F{ q } a" := (frac_auth_frag q a) (at level 10, format "◯F{ q }
 Notation "◯F a" := (frac_auth_frag 1 a) (at level 10).
 
 Section frac_auth.
-  Context {SI} {A : cmra SI}.
+  Context `{SI: indexT} {A : cmra}.
   Implicit Types a b : A.
 
   Global Instance frac_auth_auth_ne : NonExpansive (@frac_auth_auth SI A).
@@ -66,13 +66,13 @@ Section frac_auth.
 
   Lemma frac_auth_includedN n q a b : ✓{n} (●F a ⋅ ◯F{q} b) → Some b ≼{n} Some a.
   Proof. by rewrite auth_both_validN /= => -[/Some_pair_includedN [_ ?] _]. Qed.
-  Lemma frac_auth_included `{CmraDiscrete SI A} q a b :
+  Lemma frac_auth_included `{!CmraDiscrete A} q a b :
     ✓ (●F a ⋅ ◯F{q} b) → Some b ≼ Some a.
   Proof. by rewrite auth_both_valid_discrete /= => -[/Some_pair_included [_ ?] _]. Qed.
-  Lemma frac_auth_includedN_total `{CmraTotal SI A} n q a b :
+  Lemma frac_auth_includedN_total `{!CmraTotal A} n q a b :
     ✓{n} (●F a ⋅ ◯F{q} b) → b ≼{n} a.
   Proof. intros. by eapply Some_includedN_total, frac_auth_includedN. Qed.
-  Lemma frac_auth_included_total `{CmraDiscrete SI A, CmraTotal SI A} q a b :
+  Lemma frac_auth_included_total `{!CmraDiscrete A, !CmraTotal A} q a b :
     ✓ (●F a ⋅ ◯F{q} b) → b ≼ a.
   Proof. intros. by eapply Some_included_total, frac_auth_included. Qed.
 
@@ -87,7 +87,7 @@ Section frac_auth.
 
   Lemma frac_auth_frag_validN n q a : ✓{n} (◯F{q} a) ↔ ✓{n} q ∧ ✓{n} a.
   Proof. by rewrite /frac_auth_frag auth_frag_validN. Qed.
-  Lemma frac_auth_frag_valid q (a: A) : ✓ (◯F{q} a) ↔ ✓ (q: fracR SI) ∧ ✓ a.
+  Lemma frac_auth_frag_valid q (a: A) : ✓ (◯F{q} a) ↔ ✓ q ∧ ✓ a.
   Proof. by rewrite /frac_auth_frag auth_frag_valid. Qed.
 
   Lemma frac_auth_frag_op q1 q2 a1 a2 : ◯F{q1+q2} (a1 ⋅ a2) ≡ ◯F{q1} a1 ⋅ ◯F{q2} a2.
@@ -99,11 +99,11 @@ Section frac_auth.
   Proof. rewrite -frac_auth_frag_op frac_auth_frag_valid=> -[/Qp.not_add_le_l []]. Qed.
 
   Global Instance frac_auth_is_op (q q1 q2 : frac) (a a1 a2 : A) :
-    IsOp (q: fracO SI) q1 q2 → IsOp a a1 a2 → IsOp' (◯F{q} a) (◯F{q1} a1) (◯F{q2} a2).
+    IsOp q q1 q2 → IsOp a a1 a2 → IsOp' (◯F{q} a) (◯F{q1} a1) (◯F{q2} a2).
   Proof. by rewrite /IsOp' /IsOp=> /leibniz_equiv_iff -> ->. Qed.
 
   Global Instance frac_auth_is_op_core_id (q q1 q2 : frac) (a  : A) :
-    CoreId a → IsOp (q: fracO SI) q1 q2 → IsOp' (◯F{q} a) (◯F{q1} a) (◯F{q2} a).
+    CoreId a → IsOp q q1 q2 → IsOp' (◯F{q} a) (◯F{q1} a) (◯F{q2} a).
   Proof.
     rewrite /IsOp' /IsOp=> ? /leibniz_equiv_iff ->.
     by rewrite -frac_auth_frag_op -core_id_dup.
diff --git a/theories/algebra/lib/gmap_view.v b/theories/algebra/lib/gmap_view.v
index 336c5299fe650541a88ba6db1975f7a503927fae..5401b9bc1414b03310cf837c9dc9f5d31625acc6 100644
--- a/theories/algebra/lib/gmap_view.v
+++ b/theories/algebra/lib/gmap_view.v
@@ -20,17 +20,17 @@ NOTE: The API surface for [gmap_view] is experimental and subject to change.  We
 plan to add notations for authoritative elements and fragments, and hope to
 support arbitrary maps as fragments. *)
 
-Local Definition gmap_view_fragUR {SI} (K : Type) `{Countable K} (V : ofe SI) : ucmra SI :=
-  gmapUR K (prodR (dfracR SI) (agreeR V)).
+Local Definition gmap_view_fragUR `{SI: indexT} (K : Type) `{Countable K} (V : ofe) : ucmra :=
+  gmapUR K (prodR dfracR (agreeR V)).
 
 (** View relation. *)
 Section rel.
-  Context {SI} (K : Type) `{Countable K} (V : ofe SI).
-  Implicit Types (m : gmap K V) (k : K) (v : V) (n : SI).
+  Context `{SI: indexT} (K : Type) `{Countable K} (V : ofe).
+  Implicit Types (m : gmap K V) (k : K) (v : V) (n : index).
   Implicit Types (f : gmap K (dfrac * agree V)).
 
   Local Definition gmap_view_rel_raw n m f : Prop :=
-    map_Forall (λ k dv, ∃ v: V, dv.2 ≡{n}≡ to_agree v ∧ ✓ (dv.1: dfracR SI) ∧ m !! k = Some v) f.
+    map_Forall (λ k dv, ∃ v: V, dv.2 ≡{n}≡ to_agree v ∧ ✓ dv.1 ∧ m !! k = Some v) f.
 
   Local Lemma gmap_view_rel_raw_mono n1 n2 m1 m2 f1 f2 :
     gmap_view_rel_raw n1 m1 f1 →
@@ -126,16 +126,16 @@ Local Existing Instance gmap_view_rel_discrete.
 
 (** [gmap_view] is a notation to give canonical structure search the chance
 to infer the right instances (see [auth]). *)
-Notation gmap_view K V := (view (@gmap_view_rel_raw K _ _ V)).
-Definition gmap_viewO {SI} (K : Type) `{Countable K} (V : ofe SI) : ofe SI :=
+Notation gmap_view K V := (view (@gmap_view_rel_raw _ K _ V)).
+Definition gmap_viewO `{SI: indexT} (K : Type) `{Countable K} (V : ofe) : ofe :=
   viewO (gmap_view_rel K V).
-Definition gmap_viewR {SI} (K : Type) `{Countable K} (V : ofe SI) : cmra SI :=
+Definition gmap_viewR `{SI: indexT} (K : Type) `{Countable K} (V : ofe) : cmra :=
   viewR (gmap_view_rel K V).
-Definition gmap_viewUR {SI} (K : Type) `{Countable K} (V : ofe SI) : ucmra SI :=
+Definition gmap_viewUR `{SI: indexT} (K : Type) `{Countable K} (V : ofe) : ucmra :=
   viewUR (gmap_view_rel K V).
 
 Section definitions.
-  Context {SI} {K : Type} `{Countable K} {V : ofe SI}.
+  Context `{SI: indexT} {K : Type} `{Countable K} {V : ofe}.
 
   Definition gmap_view_auth (q : frac) (m : gmap K V) : gmap_viewR K V :=
     ●V{q} m.
@@ -144,7 +144,7 @@ Section definitions.
 End definitions.
 
 Section lemmas.
-  Context {SI} {K : Type} `{Countable K} {V : ofe SI}.
+  Context `{SI: indexT} {K : Type} `{Countable K} {V : ofe}.
   Implicit Types (m : gmap K V) (k : K) (q : Qp) (dq : dfrac) (v : V).
 
   Global Instance : Params (@gmap_view_auth) 5 := {}.
@@ -161,7 +161,7 @@ Section lemmas.
 
   (* Helper lemmas *)
   Local Lemma gmap_view_rel_lookup n m k dq v :
-    gmap_view_rel K V n m {[k := (dq, to_agree v)]} ↔ ✓ (dq: dfracR SI) ∧ m !! k ≡{n}≡ Some v.
+    gmap_view_rel K V n m {[k := (dq, to_agree v)]} ↔ ✓ dq ∧ m !! k ≡{n}≡ Some v.
   Proof.
     split.
     - intros Hrel.
@@ -180,7 +180,7 @@ Section lemmas.
     gmap_view_auth (p + q) m ≡ gmap_view_auth p m ⋅ gmap_view_auth q m.
   Proof. apply view_auth_frac_op. Qed.
   Global Instance gmap_view_auth_frac_is_op q q1 q2 m :
-    IsOp (q: fracO SI) q1 q2 → IsOp' (gmap_view_auth q m) (gmap_view_auth q1 m) (gmap_view_auth q2 m).
+    IsOp q q1 q2 → IsOp' (gmap_view_auth q m) (gmap_view_auth q1 m) (gmap_view_auth q2 m).
   Proof. rewrite /gmap_view_auth. apply _. Qed.
 
   Lemma gmap_view_auth_frac_op_invN n p m1 q m2 :
@@ -201,7 +201,7 @@ Section lemmas.
   Proof. rewrite gmap_view_auth_frac_valid. done. Qed.
 
   Lemma gmap_view_auth_frac_op_validN n q1 q2 m1 m2 :
-    ✓{n} (gmap_view_auth q1 m1 ⋅ gmap_view_auth q2 m2) ↔ ✓ (q1 + q2: fracR SI)%Qp ∧ m1 ≡{n}≡ m2.
+    ✓{n} (gmap_view_auth q1 m1 ⋅ gmap_view_auth q2 m2) ↔ ✓ (q1 + q2)%Qp ∧ m1 ≡{n}≡ m2.
   Proof.
     rewrite view_auth_frac_op_validN. intuition eauto using gmap_view_rel_unit.
   Qed.
@@ -211,7 +211,7 @@ Section lemmas.
     rewrite view_auth_frac_op_valid. intuition eauto using gmap_view_rel_unit.
   Qed.
   Lemma gmap_view_auth_frac_op_valid_L `{!LeibnizEquiv V} q1 q2 m1 m2 :
-    ✓ (gmap_view_auth q1 m1 ⋅ gmap_view_auth q2 m2) ↔ ✓ (q1 + q2: fracR SI)%Qp ∧ m1 = m2.
+    ✓ (gmap_view_auth q1 m1 ⋅ gmap_view_auth q2 m2) ↔ ✓ (q1 + q2)%Qp ∧ m1 = m2.
   Proof. unfold_leibniz. apply gmap_view_auth_frac_op_valid. Qed.
 
   Lemma gmap_view_auth_op_validN n m1 m2 :
@@ -221,19 +221,19 @@ Section lemmas.
     ✓ (gmap_view_auth 1 m1 ⋅ gmap_view_auth 1 m2) ↔ False.
   Proof. apply view_auth_op_valid. Qed.
 
-  Lemma gmap_view_frag_validN n k dq v : ✓{n} gmap_view_frag k dq v ↔ ✓ (dq: dfracR SI).
+  Lemma gmap_view_frag_validN n k dq v : ✓{n} gmap_view_frag k dq v ↔ ✓ dq.
   Proof.
     rewrite view_frag_validN gmap_view_rel_exists singleton_validN pair_validN.
     naive_solver.
   Qed.
-  Lemma gmap_view_frag_valid k dq v : ✓ gmap_view_frag k dq v ↔ ✓ (dq: dfracR SI).
+  Lemma gmap_view_frag_valid k dq v : ✓ gmap_view_frag k dq v ↔ ✓ dq.
   Proof.
     rewrite cmra_valid_validN. setoid_rewrite gmap_view_frag_validN.
     naive_solver eauto using zero.
   Qed.
 
   Definition gmap_view_frag_op k dq1 dq2 v :
-    gmap_view_frag k ((dq1: dfracR SI) ⋅ dq2) v ≡ (gmap_view_frag k dq1 v ⋅ gmap_view_frag k dq2 v).
+    gmap_view_frag k (dq1 ⋅ dq2) v ≡ (gmap_view_frag k dq1 v ⋅ gmap_view_frag k dq2 v).
   Proof. rewrite -view_frag_op singleton_op -pair_op agree_idemp //. Qed.
   Lemma gmap_view_frag_add k q1 q2 v :
     gmap_view_frag k (DfracOwn (q1 + q2)) v ≡
@@ -242,13 +242,13 @@ Section lemmas.
 
   Lemma gmap_view_frag_op_validN n k dq1 dq2 v1 v2 :
     ✓{n} (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ↔
-      ✓ ((dq1: dfracR SI) ⋅ dq2) ∧ v1 ≡{n}≡ v2.
+      ✓ (dq1 ⋅ dq2) ∧ v1 ≡{n}≡ v2.
   Proof.
     rewrite view_frag_validN gmap_view_rel_exists singleton_op singleton_validN.
     by rewrite -pair_op pair_validN to_agree_op_validN.
   Qed.
   Lemma gmap_view_frag_op_valid k dq1 dq2 v1 v2 :
-    ✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ↔ ✓ ((dq1: dfracR SI) ⋅ dq2) ∧ v1 ≡ v2.
+    ✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ↔ ✓ (dq1 ⋅ dq2) ∧ v1 ≡ v2.
   Proof.
     rewrite view_frag_valid. setoid_rewrite gmap_view_rel_exists.
     rewrite -cmra_valid_validN singleton_op singleton_valid.
@@ -257,12 +257,12 @@ Section lemmas.
   (* FIXME: Having a [valid_L] lemma is not consistent with [auth] and [view]; they
      have [inv_L] lemmas instead that just have an equality on the RHS. *)
   Lemma gmap_view_frag_op_valid_L `{!LeibnizEquiv V} k dq1 dq2 v1 v2 :
-    ✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ↔ ✓ ((dq1: dfracR SI) ⋅ dq2) ∧ v1 = v2.
+    ✓ (gmap_view_frag k dq1 v1 ⋅ gmap_view_frag k dq2 v2) ↔ ✓ (dq1 ⋅ dq2) ∧ v1 = v2.
   Proof. unfold_leibniz. apply gmap_view_frag_op_valid. Qed.
 
   Lemma gmap_view_both_frac_validN n q m k dq v :
     ✓{n} (gmap_view_auth q m ⋅ gmap_view_frag k dq v) ↔
-      (q ≤ 1)%Qp ∧ ✓ (dq: dfracR SI) ∧ m !! k ≡{n}≡ Some v.
+      (q ≤ 1)%Qp ∧ ✓ dq ∧ m !! k ≡{n}≡ Some v.
   Proof.
     rewrite /gmap_view_auth /gmap_view_frag.
     rewrite view_both_frac_validN gmap_view_rel_lookup.
@@ -270,11 +270,11 @@ Section lemmas.
   Qed.
   Lemma gmap_view_both_validN n m k dq v :
     ✓{n} (gmap_view_auth 1 m ⋅ gmap_view_frag k dq v) ↔
-      ✓ (dq: dfracR SI) ∧ m !! k ≡{n}≡ Some v.
+      ✓ dq ∧ m !! k ≡{n}≡ Some v.
   Proof. rewrite gmap_view_both_frac_validN. naive_solver done. Qed.
   Lemma gmap_view_both_frac_valid q m k dq v :
     ✓ (gmap_view_auth q m ⋅ gmap_view_frag k dq v) ↔
-    (q ≤ 1)%Qp ∧ ✓ (dq: dfracR SI) ∧ m !! k ≡ Some v.
+    (q ≤ 1)%Qp ∧ ✓ dq ∧ m !! k ≡ Some v.
   Proof.
     rewrite /gmap_view_auth /gmap_view_frag.
     rewrite view_both_frac_valid. setoid_rewrite gmap_view_rel_lookup.
@@ -288,23 +288,23 @@ Section lemmas.
   Qed.
   Lemma gmap_view_both_frac_valid_L `{!LeibnizEquiv V} q m k dq v :
     ✓ (gmap_view_auth q m ⋅ gmap_view_frag k dq v) ↔
-    ✓ (q: fracR SI) ∧ ✓ (dq: dfracR SI) ∧ m !! k = Some v.
+    ✓ q ∧ ✓ dq ∧ m !! k = Some v.
   Proof. unfold_leibniz. apply gmap_view_both_frac_valid. Qed.
   Lemma gmap_view_both_valid m k dq v :
     ✓ (gmap_view_auth 1 m ⋅ gmap_view_frag k dq v) ↔
-    ✓ (dq: dfracR SI) ∧ m !! k ≡ Some v.
+    ✓ dq ∧ m !! k ≡ Some v.
   Proof. rewrite gmap_view_both_frac_valid. naive_solver done. Qed.
   (* FIXME: Having a [valid_L] lemma is not consistent with [auth] and [view]; they
      have [inv_L] lemmas instead that just have an equality on the RHS. *)
   Lemma gmap_view_both_valid_L `{!LeibnizEquiv V} m k dq v :
     ✓ (gmap_view_auth 1 m ⋅ gmap_view_frag k dq v) ↔
-    ✓ (dq: dfracR SI) ∧ m !! k = Some v.
+    ✓ dq ∧ m !! k = Some v.
   Proof. unfold_leibniz. apply gmap_view_both_valid. Qed.
 
   (** Frame-preserving updates *)
   Lemma gmap_view_alloc m k dq v :
     m !! k = None →
-    ✓ (dq: dfracR SI) →
+    ✓ dq →
     gmap_view_auth 1 m ~~> gmap_view_auth 1 (<[k := v]> m) ⋅ gmap_view_frag k dq v.
   Proof.
     intros Hfresh Hdq. apply view_update_alloc=>n bf Hrel j [df va] /=.
@@ -325,7 +325,7 @@ Section lemmas.
 
   Lemma gmap_view_alloc_big m m' dq :
     m' ##ₘ m →
-    ✓ (dq: dfracR SI) →
+    ✓ dq →
     gmap_view_auth 1 m ~~>
       gmap_view_auth 1 (m' ∪ m) ⋅ ([^op map] k↦v ∈ m', gmap_view_frag k dq v).
   Proof.
@@ -404,20 +404,20 @@ Section lemmas.
   Qed.
 
   (** Typeclass instances *)
-  Global Instance gmap_view_frag_core_id k dq v : CoreId (dq: dfracR SI) → CoreId (gmap_view_frag k dq v).
+  Global Instance gmap_view_frag_core_id k dq v : CoreId dq → CoreId (gmap_view_frag k dq v).
   Proof. apply _. Qed.
 
   Global Instance gmap_view_cmra_discrete : OfeDiscrete V → CmraDiscrete (gmap_viewR K V).
   Proof. apply _. Qed.
 
   Global Instance gmap_view_frag_mut_is_op dq dq1 dq2 k v :
-    IsOp (dq: dfracR SI) dq1 dq2 →
+    IsOp dq dq1 dq2 →
     IsOp' (gmap_view_frag k dq v) (gmap_view_frag k dq1 v) (gmap_view_frag k dq2 v).
   Proof. rewrite /IsOp' /IsOp => ->. apply gmap_view_frag_op. Qed.
 End lemmas.
 
 (** Functor *)
-Program Definition gmap_viewURF {SI} (K : Type) `{Countable K} (F : oFunctor SI) : urFunctor SI := {|
+Program Definition gmap_viewURF `{SI: indexT} (K : Type) `{Countable K} (F : oFunctor) : urFunctor := {|
   urFunctor_car A B := gmap_viewUR K (oFunctor_car F A B);
   urFunctor_map A1 A2 B1 B2 fg :=
     viewO_map (rel:=gmap_view_rel K (oFunctor_car F A1 B1))
@@ -473,7 +473,7 @@ Next Obligation.
   rewrite Hagree. rewrite agree_map_to_agree. done.
 Qed.
 
-Global Instance gmap_viewURF_contractive {SI} (K : Type) `{Countable K} (F: oFunctor SI) :
+Global Instance gmap_viewURF_contractive `{SI: indexT} (K : Type) `{Countable K} (F: oFunctor) :
   oFunctorContractive F → urFunctorContractive (gmap_viewURF K F).
 Proof.
   intros ? A1 A2 B1 B2 n f g Hfg.
@@ -483,7 +483,7 @@ Proof.
     apply agreeO_map_ne, oFunctor_map_contractive. done.
 Qed.
 
-Program Definition gmap_viewRF {SI} (K : Type) `{Countable K} (F : oFunctor SI) : rFunctor SI := {|
+Program Definition gmap_viewRF `{SI: indexT} (K : Type) `{Countable K} (F : oFunctor) : rFunctor := {|
   rFunctor_car A B := gmap_viewR K (oFunctor_car F A B);
   rFunctor_map A1 A2 B1 B2 fg :=
     viewO_map (rel:=gmap_view_rel K (oFunctor_car F A1 B1))
@@ -509,8 +509,8 @@ Next Obligation.
 Qed.
 Next Obligation. intros; apply gmap_viewURF. Qed.
 
-Global Instance gmap_viewRF_contractive {SI} (K : Type) `{Countable K} (F: oFunctor SI) :
+Global Instance gmap_viewRF_contractive `{SI: indexT} (K : Type) `{Countable K} (F: oFunctor) :
   oFunctorContractive F → rFunctorContractive (gmap_viewRF K F).
 Proof. apply gmap_viewURF_contractive. Qed.
 
-Typeclasses Opaque gmap_view_auth gmap_view_frag.
+Global Typeclasses Opaque gmap_view_auth gmap_view_frag.
diff --git a/theories/algebra/lib/mono_nat.v b/theories/algebra/lib/mono_nat.v
index 5b4487c0798c5f6a39634d60fe1b344e02d69542..b8f1edf767bfae00ed0fa5c5c40350e946269e64 100644
--- a/theories/algebra/lib/mono_nat.v
+++ b/theories/algebra/lib/mono_nat.v
@@ -5,21 +5,21 @@ From iris.prelude Require Import options.
 (** Authoritative CMRA over [max_nat]. The authoritative element is a
 monotonically increasing [nat], while a fragment is a lower bound. *)
 
-Definition mono_nat SI := auth (max_natUR SI).
-Definition mono_natR SI := authR (max_natUR SI).
-Definition mono_natUR SI := authUR (max_natUR SI).
+Definition mono_nat `{SI: indexT} := auth (max_natUR).
+Definition mono_natR `{SI: indexT} := authR (max_natUR).
+Definition mono_natUR `{SI: indexT} := authUR (max_natUR).
 
 (** [mono_nat_auth] is the authoritative element. The definition includes the
 fragment at the same value so that lemma [mono_nat_included], which states that
 [mono_nat_lb n ≼ mono_nat_auth q n], does not require a frame-preserving
 update. *)
-Definition mono_nat_auth {SI} (q : Qp) (n : natO SI) : mono_nat SI :=
+Definition mono_nat_auth `{SI: indexT} (q : Qp) (n : nat) : mono_nat :=
   ●{q} MaxNat n ⋅ ◯ MaxNat n.
-Definition mono_nat_lb {SI} (n : natO SI) : mono_nat SI := ◯ MaxNat n.
+Definition mono_nat_lb `{SI: indexT} (n : nat) : mono_nat := ◯ MaxNat n.
 
 Section mono_nat.
-  Context {SI: indexT}.
-  Implicit Types (n : natO SI).
+  Context `{SI: indexT}.
+  Implicit Types (n : nat).
 
   Global Instance mono_nat_lb_core_id n : CoreId (@mono_nat_lb SI n).
   Proof. apply _. Qed.
@@ -97,4 +97,4 @@ Section mono_nat.
   Qed.
 End mono_nat.
 
-Typeclasses Opaque mono_nat_auth mono_nat_lb.
+Global Typeclasses Opaque mono_nat_auth mono_nat_lb.
diff --git a/theories/algebra/lib/ufrac_auth.v b/theories/algebra/lib/ufrac_auth.v
index 453adcd50d212322abbc2a2258145df9a2614a9f..f036202212ecf63364101f3dc18e4008c05e0b49 100644
--- a/theories/algebra/lib/ufrac_auth.v
+++ b/theories/algebra/lib/ufrac_auth.v
@@ -20,10 +20,10 @@ From iris.algebra Require Export auth frac updates local_updates.
 From iris.algebra Require Import ufrac proofmode_classes.
 From iris.prelude Require Import options.
 
-Definition ufrac_authR {SI} (A : cmra SI) : cmra SI :=
-  authR (optionUR (prodR (ufracR SI) A)).
-Definition ufrac_authUR {SI} (A : cmra SI) : ucmra SI :=
-  authUR (optionUR (prodR (ufracR SI) A)).
+Definition ufrac_authR `{SI: indexT} (A : cmra) : cmra :=
+  authR (optionUR (prodR ufracR A)).
+Definition ufrac_authUR `{SI: indexT} (A : cmra) : ucmra :=
+  authUR (optionUR (prodR ufracR A)).
 
 (** Note in the signature of [ufrac_auth_auth] and [ufrac_auth_frag] we use
 [q : Qp] instead of [q : ufrac]. This way, the API does not expose that [ufrac]
@@ -32,12 +32,12 @@ instances with carrier [Qp], namely [fracR] and [ufracR]. When writing things
 like [ufrac_auth_auth q a ∧ ✓ q] we want Coq to infer the type of [q] as [Qp]
 such that the [✓] of the default [fracR] camera is used, and not the [✓] of
 the [ufracR] camera. *)
-Definition ufrac_auth_auth {SI} {A : cmra SI} (q : Qp) (x : A) : ufrac_authR A :=
-  ● (Some (q : ufracR SI,x)).
-Definition ufrac_auth_frag {SI} {A : cmra SI} (q : Qp) (x : A) : ufrac_authR A :=
-  ◯ (Some (q : ufracR SI,x)).
+Definition ufrac_auth_auth `{SI: indexT} {A : cmra} (q : Qp) (x : A) : ufrac_authR A :=
+  ● (Some (q : ufracR,x)).
+Definition ufrac_auth_frag `{SI: indexT} {A : cmra} (q : Qp) (x : A) : ufrac_authR A :=
+  ◯ (Some (q : ufracR,x)).
 
-Typeclasses Opaque ufrac_auth_auth ufrac_auth_frag.
+Global Typeclasses Opaque ufrac_auth_auth ufrac_auth_frag.
 
 Global Instance: Params (@ufrac_auth_auth) 3 := {}.
 Global Instance: Params (@ufrac_auth_frag) 3 := {}.
@@ -46,7 +46,7 @@ Notation "●U{ q } a" := (ufrac_auth_auth q a) (at level 10, format "●U{ q }
 Notation "◯U{ q } a" := (ufrac_auth_frag q a) (at level 10, format "◯U{ q }  a").
 
 Section ufrac_auth.
-  Context {SI} {A : cmra SI}.
+  Context `{SI: indexT} {A : cmra}.
   Implicit Types a b : A.
 
   Global Instance ufrac_auth_auth_ne q : NonExpansive (@ufrac_auth_auth SI A q).
@@ -71,10 +71,9 @@ Section ufrac_auth.
   Lemma ufrac_auth_agreeN n p a b : ✓{n} (●U{p} a ⋅ ◯U{p} b) → a ≡{n}≡ b.
   Proof.
     rewrite auth_both_validN=> -[/Some_includedN [[_ ? //]|Hincl] _].
-    move: Hincl=> /pair_includedN -[/ufrac_included Hincl _].
-    specialize (Hincl SI).
+    move: Hincl=> /pair_includedN=> -[/ufrac_included Hincl _].
     by destruct (irreflexivity (<)%Qp p).
-  Qed.
+   Qed.
   Lemma ufrac_auth_agree p a b : ✓ (●U{p} a ⋅ ◯U{p} b) → a ≡ b.
   Proof.
     intros. apply equiv_dist=> n. by eapply ufrac_auth_agreeN, cmra_valid_validN.
@@ -120,11 +119,11 @@ Section ufrac_auth.
   Proof. done. Qed.
 
   Global Instance ufrac_auth_is_op q q1 q2 a a1 a2 :
-    IsOp (q: fracO SI) q1 q2 → IsOp a a1 a2 → IsOp' (◯U{q} a) (◯U{q1} a1) (◯U{q2} a2).
+    IsOp q q1 q2 → IsOp a a1 a2 → IsOp' (◯U{q} a) (◯U{q1} a1) (◯U{q2} a2).
   Proof. by rewrite /IsOp' /IsOp=> /leibniz_equiv_iff -> ->. Qed.
 
   Global Instance ufrac_auth_is_op_core_id q q1 q2 a :
-    CoreId a → IsOp (q: fracO SI) q1 q2 → IsOp' (◯U{q} a) (◯U{q1} a) (◯U{q2} a).
+    CoreId a → IsOp q q1 q2 → IsOp' (◯U{q} a) (◯U{q1} a) (◯U{q2} a).
   Proof.
     rewrite /IsOp' /IsOp=> ? /leibniz_equiv_iff ->.
     by rewrite -ufrac_auth_frag_op -core_id_dup.
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index f7759b6f4b5b17bd8cc72f60fecf61c88b984439..b4be7d70d8840ddb087688f797294696ad7e66d7 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -4,10 +4,10 @@ From iris.algebra Require Import updates local_updates big_op.
 From iris.prelude Require Import options.
 
 Section ofe.
-Context {SI} {A : ofe SI}.
+Context `{SI: indexT} {A : ofe}.
 Implicit Types l : list A.
 
-Local Instance list_dist : Dist SI (list A) := λ n, Forall2 (dist n).
+Local Instance list_dist : Dist (list A) := λ n, Forall2 (dist n).
 
 Lemma list_dist_lookup n l1 l2 : l1 ≡{n}≡ l2 ↔ ∀ i, l1 !! i ≡{n}≡ l2 !! i.
 Proof. setoid_rewrite dist_option_Forall2. apply Forall2_lookup. Qed.
@@ -49,7 +49,7 @@ Lemma list_dist_cons_inv_r n l k y :
   l ≡{n}≡ y :: k → ∃ x l', x ≡{n}≡ y ∧ l' ≡{n}≡ k ∧ l = x :: l'.
 Proof. apply Forall2_cons_inv_r. Qed.
 
-Definition list_ofe_mixin : OfeMixin SI (list A).
+Definition list_ofe_mixin : OfeMixin (list A).
 Proof.
   split.
   - intros l k. rewrite equiv_Forall2 -Forall2_forall.
@@ -127,32 +127,32 @@ End ofe.
 Global Arguments listO {_} _.
 
 (** Non-expansiveness of higher-order list functions and big-ops *)
-Global Instance list_fmap_ne {SI} {A B : ofe SI} (f : A → B) n :
+Global Instance list_fmap_ne `{SI: indexT} {A B : ofe} (f : A → B) n :
   Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (fmap (M:=list) f).
 Proof. intros Hf l k ?; by eapply Forall2_fmap, Forall2_impl; eauto. Qed.
-Global Instance list_omap_ne {SI} {A B : ofe SI} (f : A → option B) n :
+Global Instance list_omap_ne `{SI: indexT} {A B : ofe} (f : A → option B) n :
   Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (omap (M:=list) f).
 Proof.
   intros Hf. induction 1 as [|x1 x2 l1 l2 Hx Hl]; csimpl; [constructor|].
   destruct (Hf _ _ Hx); [f_equiv|]; auto.
 Qed.
-Global Instance imap_ne {SI} {A B : ofe SI} (f : nat → A → B) n :
+Global Instance imap_ne `{SI: indexT} {A B : ofe} (f : nat → A → B) n :
   (∀ i, Proper (dist n ==> dist n) (f i)) → Proper (dist n ==> dist n) (imap f).
 Proof.
   intros Hf l1 l2 Hl. revert f Hf.
   induction Hl; intros f Hf; simpl; [constructor|f_equiv; naive_solver].
 Qed.
-Global Instance list_bind_ne {SI} {A B : ofe SI} (f : A → list A) n :
+Global Instance list_bind_ne `{SI: indexT} {A B : ofe} (f : A → list A) n :
   Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (mbind f).
 Proof. induction 2; simpl; [constructor|solve_proper]. Qed.
-Global Instance list_join_ne {SI} {A : ofe SI} : NonExpansive (mjoin (M:=list) (A:=A)).
+Global Instance list_join_ne `{SI: indexT} {A : ofe} : NonExpansive (mjoin (M:=list) (A:=A)).
 Proof. induction 1; simpl; [constructor|solve_proper]. Qed.
-Global Instance zip_with_ne {SI} {A B C : ofe SI} (f : A → B → C) n :
+Global Instance zip_with_ne `{SI: indexT} {A B C : ofe} (f : A → B → C) n :
   Proper (dist n ==> dist n ==> dist n) f →
   Proper (dist n ==> dist n ==> dist n) (zip_with f).
 Proof. induction 2; destruct 1; simpl; [constructor..|f_equiv; [f_equiv|]; auto]. Qed.
 
-Lemma big_opL_ne_2 {SI} {M: ofe SI} {o: M → M → M} `{!Monoid o} {A : ofe SI} (f g : nat → A → M) l1 l2 n :
+Lemma big_opL_ne_2 `{SI: indexT} {M: ofe} {o: M → M → M} `{!Monoid o} {A : ofe} (f g : nat → A → M) l1 l2 n :
   l1 ≡{n}≡ l2 →
   (∀ k y1 y2,
     l1 !! k = Some y1 → l2 !! k = Some y2 → y1 ≡{n}≡ y2 → f k y1 ≡{n}≡ g k y2) →
@@ -165,15 +165,15 @@ Proof.
 Qed.
 
 (** Functor *)
-Lemma list_fmap_ext_ne {SI} {A} {B : ofe SI} (f g : A → B) (l : list A) n :
+Lemma list_fmap_ext_ne `{SI: indexT} {A} {B : ofe} (f g : A → B) (l : list A) n :
   (∀ x, f x ≡{n}≡ g x) → f <$> l ≡{n}≡ g <$> l.
 Proof. intros Hf. by apply Forall2_fmap, Forall_Forall2_diag, Forall_true. Qed.
-Definition listO_map {SI} {A B: ofe SI} (f : A -n> B) : listO A -n> listO B :=
+Definition listO_map `{SI: indexT} {A B: ofe} (f : A -n> B) : listO A -n> listO B :=
   OfeMor (fmap f : listO A → listO B).
 Global Instance listO_map_ne SI A B : NonExpansive (@listO_map SI A B).
 Proof. intros n f g ? l. by apply list_fmap_ext_ne. Qed.
 
-Program Definition listOF {SI} (F : oFunctor SI) : oFunctor SI := {|
+Program Definition listOF `{SI: indexT} (F : oFunctor) : oFunctor := {|
   oFunctor_car A B := listO (oFunctor_car F A B);
   oFunctor_map A1 A2 B1 B2 fg := listO_map (oFunctor_map F fg)
 |}.
@@ -189,7 +189,7 @@ Next Obligation.
   apply list_fmap_equiv_ext=>y??; apply oFunctor_map_compose.
 Qed.
 
-Global Instance listOF_contractive {SI} (F: oFunctor SI) :
+Global Instance listOF_contractive `{SI: indexT} (F: oFunctor) :
   oFunctorContractive F → oFunctorContractive (listOF F).
 Proof.
   by intros ? A1 A2 B1 B2 n f g Hfg; apply listO_map_ne, oFunctor_map_contractive.
@@ -197,7 +197,7 @@ Qed.
 
 (* CMRA. Only works if [A] has a unit! *)
 Section cmra.
-  Context {SI} {A : ucmra SI}.
+  Context `{SI: indexT} {A : ucmra}.
   Implicit Types l : list A.
   Local Arguments op _ _ !_ !_ / : simpl nomatch.
 
@@ -211,7 +211,7 @@ Section cmra.
   Local Instance list_pcore_instance : PCore (list A) := λ l, Some (core <$> l).
 
   Local Instance list_valid_instance : Valid (list A) := Forall (λ x, ✓ x).
-  Local Instance list_validN_instance : ValidN SI (list A) := λ n, Forall (λ x, ✓{n} x).
+  Local Instance list_validN_instance : ValidN (list A) := λ n, Forall (λ x, ✓{n} x).
 
   Lemma cons_valid l x : ✓ (x :: l) ↔ ✓ x ∧ ✓ l.
   Proof. apply Forall_cons. Qed.
@@ -259,7 +259,7 @@ Section cmra.
       + exists (core x :: l3); constructor; by rewrite ?cmra_core_r.
   Qed.
 
-  Definition list_cmra_mixin : CmraMixin SI (list A).
+  Definition list_cmra_mixin : CmraMixin (list A).
   Proof.
     apply cmra_total_mixin.
     - eauto.
@@ -294,17 +294,17 @@ Section cmra.
           [by inversion_clear Heq; inversion_clear Hl..|].
         exists (y1' :: l1'), (y2' :: l2'); repeat constructor; auto.
   Qed.
-  Canonical Structure listR := Cmra SI (list A) list_cmra_mixin.
+  Canonical Structure listR := Cmra (list A) list_cmra_mixin.
 
   Global Instance list_unit_instance : Unit (list A) := [].
-  Definition list_ucmra_mixin : UcmraMixin SI (list A).
+  Definition list_ucmra_mixin : UcmraMixin (list A).
   Proof.
     split.
     - constructor.
     - by intros l.
     - by constructor.
   Qed.
-  Canonical Structure listUR := Ucmra SI (list A) list_ucmra_mixin.
+  Canonical Structure listUR := Ucmra (list A) list_ucmra_mixin.
 
   Global Instance list_cmra_discrete : CmraDiscrete A → CmraDiscrete listR.
   Proof.
@@ -328,11 +328,11 @@ End cmra.
 Global Arguments listR {_} _.
 Global Arguments listUR {_} _.
 
-Global Instance list_singletonM {SI} {A : ucmra SI} : SingletonM nat A (list A) := λ n x,
+Global Instance list_singletonM `{SI: indexT} {A : ucmra} : SingletonM nat A (list A) := λ n x,
   replicate n ε ++ [x].
 
 Section properties.
-  Context {SI} {A : ucmra SI}.
+  Context `{SI: indexT} {A : ucmra}.
   Implicit Types l : list A.
   Implicit Types x y z : A.
   Local Arguments op _ _ !_ !_ / : simpl nomatch.
@@ -544,7 +544,7 @@ Section properties.
 End properties.
 
 (** Functor *)
-Global Instance list_fmap_cmra_morphism {SI} {A B : ucmra SI} (f : A → B)
+Global Instance list_fmap_cmra_morphism `{SI: indexT} {A B : ucmra} (f : A → B)
   `{!CmraMorphism f} : CmraMorphism (fmap f : list A → list B).
 Proof.
   split; try apply _.
@@ -556,7 +556,7 @@ Proof.
     by rewrite list_lookup_op !list_lookup_fmap list_lookup_op cmra_morphism_op.
 Qed.
 
-Program Definition listURF {SI} (F : urFunctor SI) : urFunctor SI := {|
+Program Definition listURF `{SI: indexT} (F : urFunctor) : urFunctor := {|
   urFunctor_car A B := listUR (urFunctor_car F A B);
   urFunctor_map A1 A2 B1 B2 fg := listO_map (urFunctor_map F fg)
 |}.
@@ -572,18 +572,18 @@ Next Obligation.
   apply list_fmap_equiv_ext=>y??; apply urFunctor_map_compose.
 Qed.
 
-Global Instance listURF_contractive {SI} (F: urFunctor SI) :
+Global Instance listURF_contractive `{SI: indexT} (F: urFunctor) :
   urFunctorContractive F → urFunctorContractive (listURF F).
 Proof.
   by intros ? A1 A2 B1 B2 n f g Hfg; apply listO_map_ne, urFunctor_map_contractive.
 Qed.
 
-Program Definition listRF {SI} (F : urFunctor SI) : rFunctor SI := {|
+Program Definition listRF `{SI: indexT} (F : urFunctor) : rFunctor := {|
   rFunctor_car A B := listR (urFunctor_car F A B);
   rFunctor_map A1 A2 B1 B2 fg := listO_map (urFunctor_map F fg)
 |}.
 Solve Obligations with (intros; apply listURF).
 
-Global Instance listRF_contractive {SI} (F : urFunctor SI):
+Global Instance listRF_contractive `{SI: indexT} (F : urFunctor):
   urFunctorContractive F → rFunctorContractive (listRF F).
 Proof. apply listURF_contractive. Qed.
diff --git a/theories/algebra/reservation_map.v b/theories/algebra/reservation_map.v
index 05ecdc42718d902863cef49737f9481fabed751a..bda407fa526fbc7f2b4eb8db31628c7138e7c2fc 100644
--- a/theories/algebra/reservation_map.v
+++ b/theories/algebra/reservation_map.v
@@ -33,21 +33,21 @@ Global Instance: Params (@ReservationMap) 1 := {}.
 Global Instance: Params (@reservation_map_data_proj) 1 := {}.
 Global Instance: Params (@reservation_map_token_proj) 1 := {}.
 
-Definition reservation_map_data {SI} {A : cmra SI} (k : positive) (a : A) : reservation_map A :=
-  ReservationMap {[ k := a ]} (ε: coPset_disjUR SI).
-Definition reservation_map_token {SI} {A : cmra SI} (E : coPset) : reservation_map A :=
+Definition reservation_map_data `{SI: indexT} {A : cmra} (k : positive) (a : A) : reservation_map A :=
+  ReservationMap {[ k := a ]} (ε: coPset_disjUR).
+Definition reservation_map_token `{SI: indexT} {A : cmra} (E : coPset) : reservation_map A :=
   ReservationMap ∅ (CoPset E).
 Global Instance: Params (@reservation_map_data) 2 := {}.
 
 (* Ofe *)
 Section ofe.
-  Context {SI} {A : ofe SI}.
+  Context `{SI: indexT} {A : ofe}.
   Implicit Types x y : reservation_map A.
 
   Local Instance reservation_map_equiv : Equiv (reservation_map A) := λ x y,
     reservation_map_data_proj x ≡ reservation_map_data_proj y ∧
     reservation_map_token_proj x = reservation_map_token_proj y.
-  Local Instance reservation_map_dist : Dist SI (reservation_map A) := λ n x y,
+  Local Instance reservation_map_dist : Dist (reservation_map A) := λ n x y,
     reservation_map_data_proj x ≡{n}≡ reservation_map_data_proj y ∧
     reservation_map_token_proj x = reservation_map_token_proj y.
 
@@ -64,7 +64,7 @@ Section ofe.
     Proper ((≡) ==> (≡)) (@reservation_map_data_proj A).
   Proof. by destruct 1. Qed.
 
-  Definition reservation_map_ofe_mixin : OfeMixin SI (reservation_map A).
+  Definition reservation_map_ofe_mixin : OfeMixin (reservation_map A).
   Proof.
     by apply (iso_ofe_mixin
       (λ x, (reservation_map_data_proj x, reservation_map_token_proj x))).
@@ -72,7 +72,7 @@ Section ofe.
   Canonical Structure reservation_mapO :=
     Ofe (reservation_map A) reservation_map_ofe_mixin.
 
-  Global Instance ReservationMap_discrete a (b: coPset_disjO SI) :
+  Global Instance ReservationMap_discrete a (b: coPset_disjO) :
     Discrete a → Discrete b → Discrete (ReservationMap a b).
   Proof. intros ?? [??] [??]; split; unshelve unfold_leibniz; [apply SI..| |];by eapply discrete. Qed.
   Global Instance reservation_map_ofe_discrete :
@@ -85,7 +85,7 @@ Global Arguments reservation_mapO {_} _.
 
 (* Camera *)
 Section cmra.
-  Context {SI} {A : cmra SI}.
+  Context `{SI: indexT} {A : cmra}.
   Implicit Types a b : A.
   Implicit Types x y : reservation_map A.
   Implicit Types k : positive.
@@ -110,7 +110,7 @@ Section cmra.
     | CoPsetBot => False
     end.
   Global Arguments reservation_map_valid_instance !_ /.
-  Local Instance reservation_map_validN_instance : ValidN SI (reservation_map A) := λ n x,
+  Local Instance reservation_map_validN_instance : ValidN (reservation_map A) := λ n x,
     match reservation_map_token_proj x with
     | CoPset E =>
       ✓{n} (reservation_map_data_proj x) ∧
@@ -120,10 +120,10 @@ Section cmra.
     end.
   Global Arguments reservation_map_validN_instance !_ /.
   Local Instance reservation_map_pcore_instance : PCore (reservation_map A) := λ x,
-    Some (ReservationMap (core (reservation_map_data_proj x)) (ε: coPset_disjUR SI)).
+    Some (ReservationMap (core (reservation_map_data_proj x)) ε).
   Local Instance reservation_map_op_instance : Op (reservation_map A) := λ x y,
     ReservationMap (reservation_map_data_proj x ⋅ reservation_map_data_proj y)
-                   ((reservation_map_token_proj x: coPset_disjUR SI) ⋅ reservation_map_token_proj y).
+                   (reservation_map_token_proj x ⋅ reservation_map_token_proj y).
 
   Definition reservation_map_valid_eq :
     valid = λ x, match reservation_map_token_proj x with
@@ -145,7 +145,7 @@ Section cmra.
   Lemma reservation_map_included x y :
     x ≼ y ↔
       reservation_map_data_proj x ≼ reservation_map_data_proj y ∧
-      (reservation_map_token_proj x: coPset_disjUR SI) ≼ reservation_map_token_proj y.
+      reservation_map_token_proj x ≼ reservation_map_token_proj y.
   Proof.
     split; [intros [[z1 z2] Hz]; split; [exists z1|exists z2]; apply Hz|].
     intros [[z1 Hz1] [z2 Hz2]]; exists (ReservationMap z1 z2); split; auto.
@@ -156,7 +156,7 @@ Section cmra.
   Lemma reservation_map_token_proj_validN n x : ✓{n} x → ✓{n} reservation_map_token_proj x.
   Proof. by destruct x as [? [?|]]=> // -[??]. Qed.
 
-  Lemma reservation_map_cmra_mixin : CmraMixin SI (reservation_map A).
+  Lemma reservation_map_cmra_mixin : CmraMixin (reservation_map A).
   Proof.
     apply cmra_total_mixin.
     - eauto.
@@ -190,7 +190,7 @@ Section cmra.
       by exists (ReservationMap m1 E1), (ReservationMap m2 E2).
   Qed.
   Canonical Structure reservation_mapR :=
-    Cmra SI (reservation_map A) reservation_map_cmra_mixin.
+    Cmra (reservation_map A) reservation_map_cmra_mixin.
 
   Global Instance reservation_map_cmra_discrete :
     CmraDiscrete A → CmraDiscrete reservation_mapR.
@@ -200,8 +200,8 @@ Section cmra.
       by intros [?%cmra_discrete_valid ?].
   Qed.
 
-  Local Instance reservation_map_empty_instance : Unit (reservation_map A) := ReservationMap ε (ε: coPset_disjUR SI).
-  Lemma reservation_map_ucmra_mixin : UcmraMixin SI (reservation_map A).
+  Local Instance reservation_map_empty_instance : Unit (reservation_map A) := ReservationMap ε ε.
+  Lemma reservation_map_ucmra_mixin : UcmraMixin (reservation_map A).
   Proof.
     split; simpl.
     - rewrite reservation_map_valid_eq /=. split; [apply ucmra_unit_valid|]. set_solver.
@@ -209,7 +209,7 @@ Section cmra.
     - do 2 constructor; [apply (core_id_core _)|done].
   Qed.
   Canonical Structure reservation_mapUR :=
-    Ucmra SI (reservation_map A) reservation_map_ucmra_mixin.
+    Ucmra (reservation_map A) reservation_map_ucmra_mixin.
 
   Global Instance reservation_map_data_core_id k a :
     CoreId a → CoreId (reservation_map_data k a).
@@ -260,7 +260,7 @@ Section cmra.
     k ∈ E → ✓ a → reservation_map_token E ~~> reservation_map_data k a.
   Proof.
     intros ??. apply cmra_total_update=> n [mf [Ef|]] //.
-    rewrite reservation_map_validN_eq /= {1}/op /cmra_op /= {1}/ucmra_op /=.
+    rewrite reservation_map_validN_eq /= {1}/op /cmra_op /=.
     case_decide; last done.
     rewrite left_id_L {1}left_id. intros [Hmf Hdisj]; split.
     - destruct (Hdisj k) as [Hmfi|]; last set_solver.
diff --git a/theories/algebra/ufrac.v b/theories/algebra/ufrac.v
index 7abbdf8d4c06dbab5cbf63f2e8962bbddd889fd6..dc4a7ea46eca91565a381b48e8bcd2b2e9031a06 100644
--- a/theories/algebra/ufrac.v
+++ b/theories/algebra/ufrac.v
@@ -10,10 +10,10 @@ infers the [frac] camera by default when using the [Qp] type. *)
 Definition ufrac := Qp.
 
 Section ufrac.
-  Context {SI : indexT}.
+  Context `{SI : indexT}.
   Implicit Types p q : ufrac.
 
-  Canonical Structure ufracO := leibnizO SI ufrac.
+  Canonical Structure ufracO := leibnizO ufrac.
 
   Local Instance ufrac_valid_instance : Valid ufrac := λ x, True.
   Local Instance ufrac_pcore_instance : PCore ufrac := λ _, None.
@@ -29,7 +29,7 @@ Section ufrac.
 
   Definition ufrac_ra_mixin : RAMixin ufrac.
   Proof. split; try apply _; try done. Qed.
-  Canonical Structure ufracR := discreteR SI ufrac ufrac_ra_mixin.
+  Canonical Structure ufracR := discreteR ufrac ufrac_ra_mixin.
 
   Global Instance ufrac_cmra_discrete : CmraDiscrete ufracR.
   Proof. apply discrete_cmra_discrete. Qed.
@@ -42,5 +42,3 @@ Section ufrac.
   Global Instance is_op_ufrac q : IsOp' q (q/2)%Qp (q/2)%Qp.
   Proof. by rewrite /IsOp' /IsOp ufrac_op' Qp.div_2. Qed.
 End ufrac.
-Arguments ufracO : clear implicits.
-Arguments ufracR : clear implicits.
diff --git a/theories/algebra/vector.v b/theories/algebra/vector.v
index d23c4d34cedd5fa60d0dc8b6c70b9d3952193e64..d896897d19d83732597aae6e5ddbeefaefa0a9c4 100644
--- a/theories/algebra/vector.v
+++ b/theories/algebra/vector.v
@@ -4,14 +4,14 @@ From iris.algebra Require Import list.
 From iris.prelude Require Import options.
 
 Section ofe.
-  Context {SI : indexT} {A : ofe SI}.
+  Context `{SI : indexT} {A : ofe}.
 
   Local Instance vec_equiv m : Equiv (vec A m) := equiv (A:=list A).
-  Local Instance vec_dist m : Dist SI (vec A m) := dist (A:=list A).
+  Local Instance vec_dist m : Dist (vec A m) := dist (A:=list A).
 
-  Definition vec_ofe_mixin m : OfeMixin SI (vec A m).
+  Definition vec_ofe_mixin m : OfeMixin (vec A m).
   Proof. by apply (iso_ofe_mixin vec_to_list). Qed.
-  Canonical Structure vecO m : ofe SI := Ofe (vec A m) (vec_ofe_mixin m).
+  Canonical Structure vecO m : ofe := Ofe (vec A m) (vec_ofe_mixin m).
 
   Global Instance list_cofe `{!Cofe A} m : Cofe (vecO m).
   Proof.
@@ -37,10 +37,10 @@ Section ofe.
 End ofe.
 
 Global Arguments vecO {_} _.
-Typeclasses Opaque vec_dist.
+Global Typeclasses Opaque vec_dist.
 
 Section proper.
-  Context {SI : indexT} {A : ofe SI}.
+  Context `{SI : indexT} {A : ofe}.
 
   Global Instance vcons_ne n :
     Proper (dist n ==> forall_relation (λ x, dist n ==> dist n)) (@vcons A).
@@ -69,28 +69,28 @@ Section proper.
 End proper.
 
 (** Functor *)
-Definition vec_map {SI : indexT} {A B : ofe SI} m (f : A → B) : vecO A m → vecO B m :=
+Definition vec_map `{SI : indexT} {A B : ofe} m (f : A → B) : vecO A m → vecO B m :=
   @vmap A B f m.
-Lemma vec_map_ext_ne {SI : indexT} {A B : ofe SI} m (f g : A → B) (v : vec A m) n :
+Lemma vec_map_ext_ne `{SI : indexT} {A B : ofe} m (f g : A → B) (v : vec A m) n :
   (∀ x, f x ≡{n}≡ g x) → vec_map m f v ≡{n}≡ vec_map m g v.
 Proof.
   intros Hf. eapply (list_fmap_ext_ne f g v) in Hf.
   by rewrite -!vec_to_list_map in Hf.
 Qed.
-Instance vec_map_ne {SI : indexT} {A B : ofe SI} m f n :
+Instance vec_map_ne `{SI : indexT} {A B : ofe} m f n :
   Proper (dist n ==> dist n) f →
   Proper (dist n ==> dist n) (@vec_map SI A B m f).
 Proof.
   intros ? v v' H. eapply list_fmap_ne in H; last done.
   by rewrite -!vec_to_list_map in H.
 Qed.
-Definition vecO_map {SI : indexT} {A B : ofe SI } m (f : A -n> B) : vecO A m -n> vecO B m :=
+Definition vecO_map `{SI : indexT} {A B : ofe } m (f : A -n> B) : vecO A m -n> vecO B m :=
   OfeMor (vec_map m f).
-Global Instance vecO_map_ne {SI : indexT} {A A'} m :
+Global Instance vecO_map_ne `{SI : indexT} {A A'} m :
   NonExpansive (@vecO_map SI A A' m).
 Proof. intros n f g ? v. by apply vec_map_ext_ne. Qed.
 
-Program Definition vecOF {SI : indexT} (F : oFunctor SI) m : oFunctor SI := {|
+Program Definition vecOF `{SI : indexT} (F : oFunctor) m : oFunctor := {|
   oFunctor_car A B := vecO (oFunctor_car F A B) m;
   oFunctor_map A1 A2 B1 B2 fg := vecO_map m (oFunctor_map F fg)
 |}.
@@ -109,7 +109,7 @@ Next Obligation.
   rewrite !vec_to_list_map. by apply: (oFunctor_map_compose (listOF F) f g f' g').
 Qed.
 
-Global Instance vecOF_contractive {SI : indexT} (F : oFunctor SI) m :
+Global Instance vecOF_contractive `{SI : indexT} (F : oFunctor) m :
   oFunctorContractive F → oFunctorContractive (vecOF F m).
 Proof.
   by intros ?? A1 A2 B1 B2 n ???; apply vecO_map_ne; first apply oFunctor_map_contractive.
diff --git a/theories/algebra/view.v b/theories/algebra/view.v
index d3962bd72fb201afda553c8d97c247423db971e9..61705f96911059d11798e3b027ca9ac21005d8c7 100644
--- a/theories/algebra/view.v
+++ b/theories/algebra/view.v
@@ -40,8 +40,8 @@ not use type classes for this purpose because cameras themselves are represented
 using canonical structures. It has proven fragile for a canonical structure
 instance to take a type class as a parameter (in this case, [viewR] would need
 to take a class with the view relation laws). *)
-Structure view_rel {SI} (A : ofe SI) (B : ucmra SI) := ViewRel {
-  view_rel_holds :> SI → A → B → Prop;
+Structure view_rel `{SI: indexT} (A : ofe) (B : ucmra) := ViewRel {
+  view_rel_holds :> index → A → B → Prop;
   view_rel_mono n1 n2 a1 a2 b1 b2 :
     view_rel_holds n1 a1 b1 →
     a1 ≡{n2}≡ a2 →
@@ -57,24 +57,24 @@ Global Arguments ViewRel {_ _ _} _ _.
 Global Arguments view_rel_holds {_ _ _} _ _ _ _.
 Global Instance: Params (@view_rel_holds) 5 := {}.
 
-Global Instance view_rel_ne {SI} {A: ofe SI} {B: ucmra SI} (rel : view_rel A B) n :
+Global Instance view_rel_ne `{SI: indexT} {A: ofe} {B: ucmra} (rel : view_rel A B) n :
   Proper (dist n ==> dist n ==> iff) (rel n).
 Proof.
   intros a1 a2 Ha b1 b2 Hb.
   split=> ?; (eapply view_rel_mono; [done|done|by rewrite Hb|done]).
 Qed.
-Global Instance view_rel_proper {SI} {A: ofe SI} {B: ucmra SI} (rel : view_rel A B) n :
+Global Instance view_rel_proper `{SI: indexT} {A: ofe} {B: ucmra} (rel : view_rel A B) n :
   Proper ((≡) ==> (≡) ==> iff) (rel n).
 Proof. intros a1 a2 Ha b1 b2 Hb. apply view_rel_ne; by apply equiv_dist. Qed.
 
-Class ViewRelDiscrete {SI} {A: ofe SI} {B: ucmra SI} (rel : view_rel A B) :=
+Class ViewRelDiscrete `{SI: indexT} {A: ofe} {B: ucmra} (rel : view_rel A B) :=
   view_rel_discrete n a b : rel zero a b → rel n a b.
 
 (** * Definition of the view camera *)
 (** To make use of the lemmas provided in this file, elements of [view] should
 always be constructed using [●V] and [◯V], and never using the constructor
 [View]. *)
-Record view {SI} {A B: ofe SI} (rel : SI → A → B → Prop) :=
+Record view `{SI: indexT} {A B: ofe} (rel : index → A → B → Prop) :=
   View { view_auth_proj : option (frac * agree A) ; view_frag_proj : B }.
 Add Printing Constructor view.
 Global Arguments View {_ _ _ _} _ _.
@@ -84,10 +84,10 @@ Global Instance: Params (@View) 4 := {}.
 Global Instance: Params (@view_auth_proj) 4 := {}.
 Global Instance: Params (@view_frag_proj) 4 := {}.
 
-Definition view_auth {SI} {A: ofe SI} {B: ucmra SI} {rel : view_rel A B} (q : Qp) (a : A) : view rel :=
+Definition view_auth `{SI: indexT} {A: ofe} {B: ucmra} {rel : view_rel A B} (q : Qp) (a : A) : view rel :=
   View (Some (q, to_agree a)) ε.
-Definition view_frag {SI} {A: ofe SI} {B: ucmra SI} {rel : view_rel A B} (b : B) : view rel := View None b.
-Typeclasses Opaque view_auth view_frag.
+Definition view_frag `{SI: indexT} {A: ofe} {B: ucmra} {rel : view_rel A B} (b : B) : view rel := View None b.
+Global Typeclasses Opaque view_auth view_frag.
 
 Global Instance: Params (@view_auth) 4 := {}.
 Global Instance: Params (@view_frag) 4 := {}.
@@ -101,7 +101,7 @@ Notation "◯V a" := (view_frag a) (at level 20).
 general version in terms of [●V] and [◯V], and because such a lemma has never
 been needed in practice. *)
 Section ofe.
-  Context {SI} {A B : ofe SI} (rel : SI → A → B → Prop).
+  Context `{SI: indexT} {A B : ofe} (rel : index → A → B → Prop).
   Implicit Types a : A.
   Implicit Types ag : option (frac * agree A).
   Implicit Types b : B.
@@ -109,7 +109,7 @@ Section ofe.
 
   Local Instance view_equiv : Equiv (view rel) := λ x y,
     view_auth_proj x ≡ view_auth_proj y ∧ view_frag_proj x ≡ view_frag_proj y.
-  Local Instance view_dist : Dist SI (view rel) := λ n x y,
+  Local Instance view_dist : Dist (view rel) := λ n x y,
     view_auth_proj x ≡{n}≡ view_auth_proj y ∧
     view_frag_proj x ≡{n}≡ view_frag_proj y.
 
@@ -128,7 +128,7 @@ Section ofe.
     Proper ((≡) ==> (≡)) (@view_frag_proj SI A B rel).
   Proof. by destruct 1. Qed.
 
-  Definition view_ofe_mixin : OfeMixin SI (view rel).
+  Definition view_ofe_mixin : OfeMixin (view rel).
   Proof. by apply (iso_ofe_mixin (λ x, (view_auth_proj x, view_frag_proj x))). Qed.
   Canonical Structure viewO := Ofe (view rel) view_ofe_mixin.
 
@@ -142,7 +142,7 @@ End ofe.
 
 (** * The camera structure *)
 Section cmra.
-  Context {SI} {A: ofe SI} {B: ucmra SI} (rel : view_rel A B).
+  Context `{SI: indexT} {A: ofe} {B: ucmra} (rel : view_rel A B).
   Implicit Types a : A.
   Implicit Types ag : option (frac * agree A).
   Implicit Types b : B.
@@ -175,14 +175,14 @@ Section cmra.
 
   Local Instance view_valid_instance : Valid (view rel) := λ x,
     match view_auth_proj x with
-    | Some (q, ag) =>
-      ✓ (q: fracR SI) ∧ (∀ n: SI, ∃ a: A, @dist SI _ _ n ag (@to_agree A a) ∧ @rel n a (view_frag_proj x))
-    | None => ∀ n: SI, ∃ a: A, @rel n a (view_frag_proj x)
+    | Some (dq, ag) =>
+      ✓ dq ∧ (∀ n, ∃ a, ag ≡{n}≡ to_agree a ∧ rel n a (view_frag_proj x))
+    | None => ∀ n, ∃ a, rel n a (view_frag_proj x)
     end.
-  Local Instance view_validN_instance : ValidN SI (view rel) := λ n x,
+  Local Instance view_validN_instance : ValidN (view rel) := λ n x,
     match view_auth_proj x with
-    | Some (q, ag) =>
-       ✓{n} q ∧ ∃ a, ag ≡{n}≡ to_agree a ∧ rel n a (view_frag_proj x)
+    | Some (dq, ag) =>
+      ✓{n} dq ∧ ∃ a, ag ≡{n}≡ to_agree a ∧ rel n a (view_frag_proj x)
     | None => ∃ a, rel n a (view_frag_proj x)
     end.
   Local Instance view_pcore_instance : PCore (view rel) := λ x,
@@ -204,7 +204,7 @@ Section cmra.
       | None => ∃ a, rel n a (view_frag_proj x)
       end := eq_refl _.
 
-  Lemma view_cmra_mixin : CmraMixin SI (view rel).
+  Lemma view_cmra_mixin : CmraMixin (view rel).
   Proof.
     apply (iso_cmra_mixin_restrict
       (λ x : option (frac * agree A) * B, View x.1 x.2)
@@ -235,7 +235,7 @@ Section cmra.
       + intros [a ?]. exists a.
         apply view_rel_mono with n a (b1 ⋅ b2); eauto using cmra_includedN_l.
   Qed.
-  Canonical Structure viewR := Cmra SI (view rel) view_cmra_mixin.
+  Canonical Structure viewR := Cmra (view rel) view_cmra_mixin.
 
   Global Instance view_auth_discrete q a :
     Discrete a → Discrete (ε : B) → Discrete (●V{q} a : view rel).
@@ -254,14 +254,14 @@ Section cmra.
   Qed.
 
   Local Instance view_empty_instance : Unit (view rel) := View ε ε.
-  Lemma view_ucmra_mixin : UcmraMixin SI (view rel).
+  Lemma view_ucmra_mixin : UcmraMixin (view rel).
   Proof.
     split; simpl.
     - rewrite view_valid_eq /=. apply view_rel_unit.
     - by intros x; constructor; rewrite /= left_id.
     - do 2 constructor; [done| apply (core_id_core _)].
   Qed.
-  Canonical Structure viewUR := Ucmra SI (view rel) view_ucmra_mixin.
+  Canonical Structure viewUR := Ucmra (view rel) view_ucmra_mixin.
 
   (** Operation *)
   Lemma view_auth_frac_op p1 p2 a : ●V{p1 + p2} a ≡ ●V{p1} a ⋅ ●V{p2} a.
@@ -270,7 +270,7 @@ Section cmra.
     by rewrite -Some_op -pair_op agree_idemp.
   Qed.
   Global Instance view_auth_frac_is_op q q1 q2 a :
-    IsOp (q: fracR SI) q1 q2 → IsOp' (●V{q} a) (●V{q1} a) (●V{q2} a).
+    IsOp q q1 q2 → IsOp' (●V{q} a) (●V{q1} a) (●V{q2} a).
   Proof. rewrite /IsOp' /IsOp => ->. by rewrite -view_auth_frac_op. Qed.
 
   Lemma view_frag_op b1 b2 : ◯V (b1 ⋅ b2) = ◯V b1 ⋅ ◯V b2.
@@ -532,22 +532,22 @@ instances of the functor structures [rFunctor] and [urFunctor]. Functors can
 only be defined for instances of [view], like [auth]. To make it more convenient
 to define functors for instances of [view], we define the map operation
 [view_map] and a bunch of lemmas about it. *)
-Definition view_map {SI} {A A' B B': ofe SI}
-    {rel : SI → A → B → Prop} {rel' : SI → A' → B' → Prop}
+Definition view_map `{SI: indexT} {A A' B B': ofe}
+    {rel : index → A → B → Prop} {rel' : index → A' → B' → Prop}
     (f : A → A') (g : B → B') (x : view rel) : view rel' :=
   View (prod_map id (agree_map f) <$> view_auth_proj x) (g (view_frag_proj x)).
-Lemma view_map_id {SI} {A B: ofe SI} {rel : SI → A → B → Prop} (x : view rel) :
+Lemma view_map_id `{SI: indexT} {A B: ofe} {rel : index → A → B → Prop} (x : view rel) :
   view_map id id x = x.
 Proof. destruct x as [[[]|] ]; by rewrite // /view_map /= agree_map_id. Qed.
-Lemma view_map_compose {SI} {A A' A'' B B' B'': ofe SI}
-    {rel : SI → A → B → Prop} {rel' : SI → A' → B' → Prop}
-    {rel'' : SI → A'' → B'' → Prop}
+Lemma view_map_compose `{SI: indexT} {A A' A'' B B' B'': ofe}
+    {rel : index → A → B → Prop} {rel' : index → A' → B' → Prop}
+    {rel'' : index → A'' → B'' → Prop}
     (f1 : A → A') (f2 : A' → A'') (g1 : B → B') (g2 : B' → B'') (x : view rel) :
   view_map (f2 ∘ f1) (g2 ∘ g1) x
   =@{view rel''} view_map f2 g2 (view_map (rel':=rel') f1 g1 x).
 Proof. destruct x as [[[]|] ];  by rewrite // /view_map /= agree_map_compose. Qed.
-Lemma view_map_ext {SI} {A A' B B' : ofe SI}
-    {rel : SI → A → B → Prop} {rel' : SI → A' → B' → Prop}
+Lemma view_map_ext `{SI: indexT} {A A' B B' : ofe}
+    {rel : index → A → B → Prop} {rel' : index → A' → B' → Prop}
     (f1 f2 : A → A') (g1 g2 : B → B')
     `{!NonExpansive f1, !NonExpansive g1} (x : view rel) :
   (∀ a, f1 a ≡ f2 a) → (∀ b, g1 b ≡ g2 b) →
@@ -556,8 +556,8 @@ Proof.
   intros. constructor; simpl; [|by auto].
   apply option_fmap_equiv_ext=> a; by rewrite /prod_map /= agree_map_ext.
 Qed.
-Global Instance view_map_ne {SI} {A A' B B' : ofe SI}
-    {rel : SI → A → B → Prop} {rel' : SI → A' → B' → Prop}
+Global Instance view_map_ne `{SI: indexT} {A A' B B' : ofe}
+    {rel : index → A → B → Prop} {rel' : index → A' → B' → Prop}
     (f : A → A') (g : B → B') `{Hf : !NonExpansive f, Hg : !NonExpansive g} :
   NonExpansive (view_map (rel':=rel') (rel:=rel) f g).
 Proof.
@@ -566,19 +566,19 @@ Proof.
   apply prod_map_ne; [done| |done]. by apply agree_map_ne.
 Qed.
 
-Definition viewO_map {SI} {A A' B B' : ofe SI}
-    {rel : SI → A → B → Prop} {rel' : SI → A' → B' → Prop}
+Definition viewO_map `{SI: indexT} {A A' B B' : ofe}
+    {rel : index → A → B → Prop} {rel' : index → A' → B' → Prop}
     (f : A -n> A') (g : B -n> B') : viewO rel -n> viewO rel' :=
   OfeMor (view_map f g).
-Lemma viewO_map_ne {SI} {A A' B B' : ofe SI}
-    {rel : SI → A → B → Prop} {rel' : SI → A' → B' → Prop} :
+Lemma viewO_map_ne `{SI: indexT} {A A' B B' : ofe}
+    {rel : index → A → B → Prop} {rel' : index → A' → B' → Prop} :
   NonExpansive2 (viewO_map (rel:=rel) (rel':=rel')).
 Proof.
   intros n f f' Hf g g' Hg [[[p ag]|] bf]; split=> //=.
   do 2 f_equiv. by apply agreeO_map_ne.
 Qed.
 
-Lemma view_map_cmra_morphism {SI} {A A' : ofe SI} {B B': ucmra SI}
+Lemma view_map_cmra_morphism `{SI: indexT} {A A' : ofe} {B B': ucmra}
     {rel : view_rel A B} {rel' : view_rel A' B'}
     (f : A → A') (g : B → B') `{!NonExpansive f, !CmraMorphism g} :
   (∀ n a b, rel n a b → rel' n (f a) (g b)) →