diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index ad8dc5a553afd649a2abd6624fad1373b68e2762..28cf7fdec5584dafc775e05be9faf266d4da18a4 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -249,7 +249,7 @@ Lemma to_agree_uninjI {M} x : ✓ x ⊢@{uPredI M} ∃ a, to_agree a ≡ x.
 Proof. uPred.unseal. split=> n y _. exact: to_agree_uninjN. Qed.
 End agree.
 
-Instance: Params (@to_agree) 1.
+Instance: Params (@to_agree) 1 := {}.
 Arguments agreeC : clear implicits.
 Arguments agreeR : clear implicits.
 
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index eb395222227a127dd426d50a2f7587cca5b699e2..7bfb354c4d0f3aaedbcc17d7425799bd02f710a0 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -8,9 +8,9 @@ Add Printing Constructor auth.
 Arguments Auth {_} _ _.
 Arguments authoritative {_} _.
 Arguments auth_own {_} _.
-Instance: Params (@Auth) 1.
-Instance: Params (@authoritative) 1.
-Instance: Params (@auth_own) 1.
+Instance: Params (@Auth) 1 := {}.
+Instance: Params (@authoritative) 1 := {}.
+Instance: Params (@auth_own) 1 := {}.
 Notation "â—¯ a" := (Auth None a) (at level 20).
 Notation "● a" := (Auth (Excl' a) ε) (at level 20).
 
diff --git a/theories/algebra/big_op.v b/theories/algebra/big_op.v
index 8d9110eff060555e812daefbe878030a313d0b69..be8030e1d12311175828a5016991dfb6bc6c41e1 100644
--- a/theories/algebra/big_op.v
+++ b/theories/algebra/big_op.v
@@ -25,7 +25,7 @@ Fixpoint big_opL `{Monoid M o} {A} (f : nat → A → M) (xs : list A) : M :=
   | [] => monoid_unit
   | x :: xs => o (f 0 x) (big_opL (λ n, f (S n)) xs)
   end.
-Instance: Params (@big_opL) 4.
+Instance: Params (@big_opL) 4 := {}.
 Arguments big_opL {M} o {_ A} _ !_ /.
 Typeclasses Opaque big_opL.
 Notation "'[^' o 'list]' k ↦ x ∈ l , P" := (big_opL o (λ k x, P) l)
@@ -37,7 +37,7 @@ Notation "'[^' o 'list]' x ∈ l , P" := (big_opL o (λ _ x, P) l)
 
 Definition big_opM `{Monoid M o} `{Countable K} {A} (f : K → A → M)
     (m : gmap K A) : M := big_opL o (λ _, curry f) (map_to_list m).
-Instance: Params (@big_opM) 7.
+Instance: Params (@big_opM) 7 := {}.
 Arguments big_opM {M} o {_ K _ _ A} _ _ : simpl never.
 Typeclasses Opaque big_opM.
 Notation "'[^' o 'map]' k ↦ x ∈ m , P" := (big_opM o (λ k x, P) m)
@@ -49,7 +49,7 @@ Notation "'[^' o 'map]' x ∈ m , P" := (big_opM o (λ _ x, P) m)
 
 Definition big_opS `{Monoid M o} `{Countable A} (f : A → M)
   (X : gset A) : M := big_opL o (λ _, f) (elements X).
-Instance: Params (@big_opS) 6.
+Instance: Params (@big_opS) 6 := {}.
 Arguments big_opS {M} o {_ A _ _} _ _ : simpl never.
 Typeclasses Opaque big_opS.
 Notation "'[^' o 'set]' x ∈ X , P" := (big_opS o (λ x, P) X)
@@ -58,7 +58,7 @@ Notation "'[^' o 'set]' x ∈ X , P" := (big_opS o (λ x, P) X)
 
 Definition big_opMS `{Monoid M o} `{Countable A} (f : A → M)
   (X : gmultiset A) : M := big_opL o (λ _, f) (elements X).
-Instance: Params (@big_opMS) 7.
+Instance: Params (@big_opMS) 7 := {}.
 Arguments big_opMS {M} o {_ A _ _} _ _ : simpl never.
 Typeclasses Opaque big_opMS.
 Notation "'[^' o 'mset]' x ∈ X , P" := (big_opMS o (λ x, P) X)
@@ -417,7 +417,7 @@ Section homomorphisms.
   [RewriteRelation] instance. For the purpose of this section, we want to
   rewrite with arbitrary relations, so we declare any relation to be a
   [RewriteRelation]. *)
-  Local Instance: ∀ {A} (R : relation A), RewriteRelation R.
+  Local Instance: ∀ {A} (R : relation A), RewriteRelation R := {}.
 
   Lemma big_opL_commute {A} (h : M1 → M2) `{!MonoidHomomorphism o1 o2 R h}
       (f : nat → A → M1) l :
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 335b60246f8ade4c016633b8161a70b4aa06445e..d4418c515e2d989ff513ce006dfa32448a8228e1 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -4,11 +4,11 @@ Set Default Proof Using "Type".
 
 Class PCore (A : Type) := pcore : A → option A.
 Hint Mode PCore ! : typeclass_instances.
-Instance: Params (@pcore) 2.
+Instance: Params (@pcore) 2 := {}.
 
 Class Op (A : Type) := op : A → A → A.
 Hint Mode Op ! : typeclass_instances.
-Instance: Params (@op) 2.
+Instance: Params (@op) 2 := {}.
 Infix "â‹…" := op (at level 50, left associativity) : stdpp_scope.
 Notation "(â‹…)" := op (only parsing) : stdpp_scope.
 
@@ -21,23 +21,23 @@ Definition included `{Equiv A, Op A} (x y : A) := ∃ z, y ≡ x ⋅ z.
 Infix "≼" := included (at level 70) : stdpp_scope.
 Notation "(≼)" := included (only parsing) : stdpp_scope.
 Hint Extern 0 (_ ≼ _) => reflexivity : core.
-Instance: Params (@included) 3.
+Instance: Params (@included) 3 := {}.
 
 Class ValidN (A : Type) := validN : nat → A → Prop.
 Hint Mode ValidN ! : typeclass_instances.
-Instance: Params (@validN) 3.
+Instance: Params (@validN) 3 := {}.
 Notation "✓{ n } x" := (validN n x)
   (at level 20, n at next level, format "✓{ n }  x").
 
 Class Valid (A : Type) := valid : A → Prop.
 Hint Mode Valid ! : typeclass_instances.
-Instance: Params (@valid) 2.
+Instance: Params (@valid) 2 := {}.
 Notation "✓ x" := (valid x) (at level 20) : stdpp_scope.
 
 Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := ∃ z, y ≡{n}≡ x ⋅ z.
 Notation "x ≼{ n } y" := (includedN n x y)
   (at level 70, n at next level, format "x  ≼{ n }  y") : stdpp_scope.
-Instance: Params (@includedN) 4.
+Instance: Params (@includedN) 4 := {}.
 Hint Extern 0 (_ ≼{_} _) => reflexivity : core.
 
 Section mixin.
@@ -147,27 +147,27 @@ Infix "â‹…?" := opM (at level 50, left associativity) : stdpp_scope.
 Class CoreId {A : cmraT} (x : A) := core_id : pcore x ≡ Some x.
 Arguments core_id {_} _ {_}.
 Hint Mode CoreId + ! : typeclass_instances.
-Instance: Params (@CoreId) 1.
+Instance: Params (@CoreId) 1 := {}.
 
 (** * Exclusive elements (i.e., elements that cannot have a frame). *)
 Class Exclusive {A : cmraT} (x : A) := exclusive0_l y : ✓{0} (x ⋅ y) → False.
 Arguments exclusive0_l {_} _ {_} _ _.
 Hint Mode Exclusive + ! : typeclass_instances.
-Instance: Params (@Exclusive) 1.
+Instance: Params (@Exclusive) 1 := {}.
 
 (** * Cancelable elements. *)
 Class Cancelable {A : cmraT} (x : A) :=
   cancelableN n y z : ✓{n}(x ⋅ y) → x ⋅ y ≡{n}≡ x ⋅ z → y ≡{n}≡ z.
 Arguments cancelableN {_} _ {_} _ _ _ _.
 Hint Mode Cancelable + ! : typeclass_instances.
-Instance: Params (@Cancelable) 1.
+Instance: Params (@Cancelable) 1 := {}.
 
 (** * Identity-free elements. *)
 Class IdFree {A : cmraT} (x : A) :=
   id_free0_r y : ✓{0}x → x ⋅ y ≡{0}≡ x → False.
 Arguments id_free0_r {_} _ {_} _ _.
 Hint Mode IdFree + ! : typeclass_instances.
-Instance: Params (@IdFree) 1.
+Instance: Params (@IdFree) 1 := {}.
 
 (** * CMRAs whose core is total *)
 Class CmraTotal (A : cmraT) := cmra_total (x : A) : is_Some (pcore x).
@@ -177,7 +177,7 @@ Hint Mode CmraTotal ! : typeclass_instances.
 core. *)
 Class Core (A : Type) := core : A → A.
 Hint Mode Core ! : typeclass_instances.
-Instance: Params (@core) 2.
+Instance: Params (@core) 2 := {}.
 
 Instance core' `{PCore A} : Core A := λ x, default x (pcore x).
 Arguments core' _ _ _ /.
@@ -779,7 +779,7 @@ Structure rFunctor := RFunctor {
     CmraMorphism (rFunctor_map fg)
 }.
 Existing Instances rFunctor_ne rFunctor_mor.
-Instance: Params (@rFunctor_map) 5.
+Instance: Params (@rFunctor_map) 5 := {}.
 
 Delimit Scope rFunctor_scope with RF.
 Bind Scope rFunctor_scope with rFunctor.
@@ -812,7 +812,7 @@ Structure urFunctor := URFunctor {
     CmraMorphism (urFunctor_map fg)
 }.
 Existing Instances urFunctor_ne urFunctor_mor.
-Instance: Params (@urFunctor_map) 5.
+Instance: Params (@urFunctor_map) 5 := {}.
 
 Delimit Scope urFunctor_scope with URF.
 Bind Scope urFunctor_scope with urFunctor.
diff --git a/theories/algebra/cofe_solver.v b/theories/algebra/cofe_solver.v
index 010d4afe218775ec768a24b23e288f5db7fd1ca7..b18a584e96f871943021fa1cac3b0bf847d91c89 100644
--- a/theories/algebra/cofe_solver.v
+++ b/theories/algebra/cofe_solver.v
@@ -151,7 +151,7 @@ Qed.
 Program Definition embed (k : nat) (x : A k) : T :=
   {| tower_car n := embed_coerce n x |}.
 Next Obligation. intros k x i. apply g_embed_coerce. Qed.
-Instance: Params (@embed) 1.
+Instance: Params (@embed) 1 := {}.
 Instance embed_ne k : NonExpansive (embed k).
 Proof. by intros n x y Hxy i; rewrite /= Hxy. Qed.
 Definition embed' (k : nat) : A k -n> T := CofeMor (embed k).
diff --git a/theories/algebra/csum.v b/theories/algebra/csum.v
index cab3953aa4b9a7b85f613fdd5ec9109e585536e2..de491b25b91ecd6f606337adfe9549938c1b5654 100644
--- a/theories/algebra/csum.v
+++ b/theories/algebra/csum.v
@@ -17,9 +17,9 @@ Arguments Cinl {_ _} _.
 Arguments Cinr {_ _} _.
 Arguments CsumBot {_ _}.
 
-Instance: Params (@Cinl) 2.
-Instance: Params (@Cinr) 2.
-Instance: Params (@CsumBot) 2.
+Instance: Params (@Cinl) 2 := {}.
+Instance: Params (@Cinr) 2 := {}.
+Instance: Params (@CsumBot) 2 := {}.
 
 Instance maybe_Cinl {A B} : Maybe (@Cinl A B) := λ x,
   match x with Cinl a => Some a | _ => None end.
@@ -119,7 +119,7 @@ Definition csum_map {A A' B B'} (fA : A → A') (fB : B → B')
   | Cinr b => Cinr (fB b)
   | CsumBot => CsumBot
   end.
-Instance: Params (@csum_map) 4.
+Instance: Params (@csum_map) 4 := {}.
 
 Lemma csum_map_id {A B} (x : csum A B) : csum_map id id x = x.
 Proof. by destruct x. Qed.
diff --git a/theories/algebra/excl.v b/theories/algebra/excl.v
index 8eff76e1a4f775dc050026644f48ba302a5a19f1..849a8ab8ea84129a09302cd5837a1e5b0df92645 100644
--- a/theories/algebra/excl.v
+++ b/theories/algebra/excl.v
@@ -10,8 +10,8 @@ Inductive excl (A : Type) :=
 Arguments Excl {_} _.
 Arguments ExclBot {_}.
 
-Instance: Params (@Excl) 1.
-Instance: Params (@ExclBot) 1.
+Instance: Params (@Excl) 1 := {}.
+Instance: Params (@ExclBot) 1 := {}.
 
 Notation excl' A := (option (excl A)).
 Notation Excl' x := (Some (Excl x)).
diff --git a/theories/algebra/frac_auth.v b/theories/algebra/frac_auth.v
index 08fc6f9e00c3905e205bfdb7ceef0aa23d2be73f..30cf54715ea4e496fb14f3dc014fd93ce8b6e58d 100644
--- a/theories/algebra/frac_auth.v
+++ b/theories/algebra/frac_auth.v
@@ -14,8 +14,8 @@ Definition frac_auth_frag {A : cmraT} (q : frac) (x : A) : frac_authR A :=
 
 Typeclasses Opaque frac_auth_auth frac_auth_frag.
 
-Instance: Params (@frac_auth_auth) 1.
-Instance: Params (@frac_auth_frag) 2.
+Instance: Params (@frac_auth_auth) 1 := {}.
+Instance: Params (@frac_auth_frag) 2 := {}.
 
 Notation "●! a" := (frac_auth_auth a) (at level 10).
 Notation "â—¯!{ q } a" := (frac_auth_frag q a) (at level 10, format "â—¯!{ q }  a").
diff --git a/theories/algebra/functions.v b/theories/algebra/functions.v
index e3c368d1ac93da666e9cb5beb6b2e5f6f8007a4d..4ace8f8f7f88b43f6c969ebf5107126deff23b6d 100644
--- a/theories/algebra/functions.v
+++ b/theories/algebra/functions.v
@@ -6,11 +6,11 @@ Set Default Proof Using "Type".
 Definition ofe_fun_insert `{EqDecision A} {B : A → ofeT}
     (x : A) (y : B x) (f : ofe_fun B) : ofe_fun B := λ x',
   match decide (x = x') with left H => eq_rect _ B y _ H | right _ => f x' end.
-Instance: Params (@ofe_fun_insert) 5.
+Instance: Params (@ofe_fun_insert) 5 := {}.
 
 Definition ofe_fun_singleton `{EqDecision A} {B : A → ucmraT}
   (x : A) (y : B x) : ofe_fun B := ofe_fun_insert x y ε.
-Instance: Params (@ofe_fun_singleton) 5.
+Instance: Params (@ofe_fun_singleton) 5 := {}.
 
 Section ofe.
   Context `{Heqdec : EqDecision A} {B : A → ofeT}.
diff --git a/theories/algebra/local_updates.v b/theories/algebra/local_updates.v
index 32479f7998febcf33d80e75286fbf4b0e8cb1a35..78cf251331231b7d58a43e823bef4c9f58e56822 100644
--- a/theories/algebra/local_updates.v
+++ b/theories/algebra/local_updates.v
@@ -4,7 +4,7 @@ Set Default Proof Using "Type".
 (** * Local updates *)
 Definition local_update {A : cmraT} (x y : A * A) := ∀ n mz,
   ✓{n} x.1 → x.1 ≡{n}≡ x.2 ⋅? mz → ✓{n} y.1 ∧ y.1 ≡{n}≡ y.2 ⋅? mz.
-Instance: Params (@local_update) 1.
+Instance: Params (@local_update) 1 := {}.
 Infix "~l~>" := local_update (at level 70).
 
 Section updates.
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 3c095092e3c1c9155c9eda102c04b5a43844a367..d83c2b333b2acf02c7428e1a3705626c02f02cff 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -13,7 +13,7 @@ Set Primitive Projections.
 
 (** Unbundeled version *)
 Class Dist A := dist : nat → relation A.
-Instance: Params (@dist) 3.
+Instance: Params (@dist) 3 := {}.
 Notation "x ≡{ n }≡ y" := (dist n x y)
   (at level 70, n at next level, format "x  ≡{ n }≡  y").
 Notation "x ≡{ n }@{ A }≡ y" := (dist (A:=A) n x y)
@@ -102,7 +102,7 @@ Hint Extern 1 (_ ≡{_}≡ _) => apply equiv_dist; assumption : core.
 Class Discrete {A : ofeT} (x : A) := discrete y : x ≡{0}≡ y → x ≡ y.
 Arguments discrete {_} _ {_} _ _.
 Hint Mode Discrete + ! : typeclass_instances.
-Instance: Params (@Discrete) 1.
+Instance: Params (@Discrete) 1 := {}.
 
 Class OfeDiscrete (A : ofeT) := ofe_discrete_discrete (x : A) :> Discrete x.
 
@@ -573,13 +573,13 @@ Instance ofe_mor_inhabited {A B : ofeT} `{Inhabited B} :
 
 (** Identity and composition and constant function *)
 Definition cid {A} : A -n> A := CofeMor id.
-Instance: Params (@cid) 1.
+Instance: Params (@cid) 1 := {}.
 Definition cconst {A B : ofeT} (x : B) : A -n> B := CofeMor (const x).
-Instance: Params (@cconst) 2.
+Instance: Params (@cconst) 2 := {}.
 
 Definition ccompose {A B C}
   (f : B -n> C) (g : A -n> B) : A -n> C := CofeMor (f ∘ g).
-Instance: Params (@ccompose) 3.
+Instance: Params (@ccompose) 3 := {}.
 Infix "â—Ž" := ccompose (at level 40, left associativity).
 Global Instance ccompose_ne {A B C} :
   NonExpansive2 (@ccompose A B C).
@@ -676,7 +676,7 @@ Structure cFunctor := CFunctor {
     cFunctor_map (f◎g, g'◎f') x ≡ cFunctor_map (g,g') (cFunctor_map (f,f') x)
 }.
 Existing Instance cFunctor_ne.
-Instance: Params (@cFunctor_map) 5.
+Instance: Params (@cFunctor_map) 5 := {}.
 
 Delimit Scope cFunctor_scope with CF.
 Bind Scope cFunctor_scope with cFunctor.
@@ -995,7 +995,7 @@ Record later (A : Type) : Type := Next { later_car : A }.
 Add Printing Constructor later.
 Arguments Next {_} _.
 Arguments later_car {_} _.
-Instance: Params (@Next) 1.
+Instance: Params (@Next) 1 := {}.
 
 Section later.
   Context {A : ofeT}.
diff --git a/theories/algebra/sts.v b/theories/algebra/sts.v
index f05fe45ed28888d99fc60a0c1f829633ea22f209..0e6442a92213d68000f05c73bf87660ecae604ee 100644
--- a/theories/algebra/sts.v
+++ b/theories/algebra/sts.v
@@ -284,9 +284,9 @@ Section sts_definitions.
   Definition sts_frag_up (s : sts.state sts) (T : sts.tokens sts) : stsR sts :=
     sts_frag (sts.up s T) T.
 End sts_definitions.
-Instance: Params (@sts_auth) 2.
-Instance: Params (@sts_frag) 1.
-Instance: Params (@sts_frag_up) 2.
+Instance: Params (@sts_auth) 2 := {}.
+Instance: Params (@sts_frag) 1 := {}.
+Instance: Params (@sts_frag_up) 2 := {}.
 
 Section stsRA.
 Import sts.
diff --git a/theories/algebra/updates.v b/theories/algebra/updates.v
index e9570d8efa256894b3f6a82cc88a50c9665dc02b..790017571c14fd552c363d01d69354a15d4ed0c2 100644
--- a/theories/algebra/updates.v
+++ b/theories/algebra/updates.v
@@ -8,13 +8,13 @@ Set Default Proof Using "Type".
 *)
 Definition cmra_updateP {A : cmraT} (x : A) (P : A → Prop) := ∀ n mz,
   ✓{n} (x ⋅? mz) → ∃ y, P y ∧ ✓{n} (y ⋅? mz).
-Instance: Params (@cmra_updateP) 1.
+Instance: Params (@cmra_updateP) 1 := {}.
 Infix "~~>:" := cmra_updateP (at level 70).
 
 Definition cmra_update {A : cmraT} (x y : A) := ∀ n mz,
   ✓{n} (x ⋅? mz) → ✓{n} (y ⋅? mz).
 Infix "~~>" := cmra_update (at level 70).
-Instance: Params (@cmra_update) 1.
+Instance: Params (@cmra_update) 1 := {}.
 
 Section updates.
 Context {A : cmraT}.
diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v
index bd849ac1fe365dab99912240c7d10b3109e16fe5..09e64079fc0000e6398afedb13fad4ec181eb674 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -55,9 +55,9 @@ Section definitions.
 End definitions.
 
 Typeclasses Opaque auth_own auth_inv auth_ctx.
-Instance: Params (@auth_own) 4.
-Instance: Params (@auth_inv) 5.
-Instance: Params (@auth_ctx) 7.
+Instance: Params (@auth_own) 4 := {}.
+Instance: Params (@auth_inv) 5 := {}.
+Instance: Params (@auth_ctx) 7 := {}.
 
 Section auth.
   Context `{invG Σ, authG Σ A}.
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 597f175ab0b6ee5cf9ecbe70cc04bdf89ed9f830..9e50462193999332963bb000f4e793d381f55833 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -40,10 +40,10 @@ Section box_defs.
                          inv N (slice_inv γ (Φ γ)))%I.
 End box_defs.
 
-Instance: Params (@box_own_prop) 3.
-Instance: Params (@slice_inv) 3.
-Instance: Params (@slice) 5.
-Instance: Params (@box) 5.
+Instance: Params (@box_own_prop) 3 := {}.
+Instance: Params (@slice_inv) 3 := {}.
+Instance: Params (@slice) 5 := {}.
+Instance: Params (@box) 5 := {}.
 
 Section box.
 Context `{invG Σ, boxG Σ} (N : namespace).
diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index e2f20276dc2cc0aa22b2dcf5480efbe575217310..8239e7e3bb857b64b1388edc94f76d7c69362ecf 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -20,7 +20,7 @@ Section defs.
     (∃ P', □ ▷ (P ↔ P') ∗ inv N (P' ∨ cinv_own γ 1%Qp))%I.
 End defs.
 
-Instance: Params (@cinv) 5.
+Instance: Params (@cinv) 5 := {}.
 
 Section proofs.
   Context `{invG Σ, cinvG Σ}.
@@ -108,7 +108,7 @@ Section proofs.
     iIntros "!> HP". iApply "H"; auto.
   Qed.
 
-  Global Instance into_inv_cinv N γ P : IntoInv (cinv N γ P) N.
+  Global Instance into_inv_cinv N γ P : IntoInv (cinv N γ P) N := {}.
 
   Global Instance into_acc_cinv E N γ P p :
     IntoAcc (X:=unit) (cinv N γ P)
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 1405eaf7860b0a2c38ac52b3d33f940f85427139..ae1ffaf5f65f3494eca2beede50014e1a0326dc2 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/theories/base_logic/lib/invariants.v
@@ -12,7 +12,7 @@ Definition inv_def `{invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
 Definition inv_aux : seal (@inv_def). by eexists. Qed.
 Definition inv {Σ i} := inv_aux.(unseal) Σ i.
 Definition inv_eq : @inv = @inv_def := inv_aux.(seal_eq).
-Instance: Params (@inv) 3.
+Instance: Params (@inv) 3 := {}.
 Typeclasses Opaque inv.
 
 Section inv.
@@ -107,7 +107,7 @@ Proof.
   by rewrite left_id_L.
 Qed.
 
-Global Instance into_inv_inv N P : IntoInv (inv N P) N.
+Global Instance into_inv_inv N P : IntoInv (inv N P) N := {}.
 
 Global Instance into_acc_inv E N P :
   IntoAcc (X:=unit) (inv N P) 
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index beaf8ebfe54d0ba730328d21e212bed70a651000..b39356a19f3da98cd3469720296938eefcb99415 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -26,7 +26,7 @@ Section defs.
           inv N (P ∗ own p (CoPset ∅, GSet {[i]}) ∨ na_own p {[i]}))%I.
 End defs.
 
-Instance: Params (@na_inv) 3.
+Instance: Params (@na_inv) 3 := {}.
 Typeclasses Opaque na_own na_inv.
 
 Section proofs.
@@ -111,7 +111,7 @@ Section proofs.
     - iDestruct (na_own_disjoint with "Htoki Htoki2") as %?. set_solver.
   Qed.
 
-  Global Instance into_inv_na p N P : IntoInv (na_inv p N P) N.
+  Global Instance into_inv_na p N P : IntoInv (na_inv p N P) N := {}.
 
   Global Instance into_acc_na p F E N P :
     IntoAcc (X:=unit) (na_inv p N P)
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 9f570de8b87c38d2b37a22d43fc01210c4ab7666..e55af99d318d16718787b9d827ed3b7cb76bc4bf 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -49,14 +49,14 @@ Ltac solve_inG :=
 (** * Definition of the connective [own] *)
 Definition iRes_singleton `{i : inG Σ A} (γ : gname) (a : A) : iResUR Σ :=
   ofe_fun_singleton (inG_id i) {[ γ := cmra_transport inG_prf a ]}.
-Instance: Params (@iRes_singleton) 4.
+Instance: Params (@iRes_singleton) 4 := {}.
 
 Definition own_def `{inG Σ A} (γ : gname) (a : A) : iProp Σ :=
   uPred_ownM (iRes_singleton γ a).
 Definition own_aux : seal (@own_def). by eexists. Qed.
 Definition own {Σ A i} := own_aux.(unseal) Σ A i.
 Definition own_eq : @own = @own_def := own_aux.(seal_eq).
-Instance: Params (@own) 4.
+Instance: Params (@own) 4 := {}.
 Typeclasses Opaque own.
 
 (** * Properties about ghost ownership *)
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index c8ee4d412e4f54b7c796e81be8b1fed293152e78..bc0a581d9ccc9d3c7d93fc9cfd8f401c24c371cc 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -21,7 +21,7 @@ Definition saved_anything_own `{savedAnythingG Σ F}
     (γ : gname) (x : F (iProp Σ)) : iProp Σ :=
   own γ (to_agree $ (cFunctor_map F (iProp_fold, iProp_unfold) x)).
 Typeclasses Opaque saved_anything_own.
-Instance: Params (@saved_anything_own) 4.
+Instance: Params (@saved_anything_own) 4 := {}.
 
 Section saved_anything.
   Context `{savedAnythingG Σ F}.
diff --git a/theories/base_logic/lib/sts.v b/theories/base_logic/lib/sts.v
index 0d8e8ced6b615324537aded18038145a6d64606b..368cb41ed00c050203e744997c4e141b0a388006 100644
--- a/theories/base_logic/lib/sts.v
+++ b/theories/base_logic/lib/sts.v
@@ -51,10 +51,10 @@ Section definitions.
   Proof. apply _. Qed.
 End definitions.
 
-Instance: Params (@sts_inv) 4.
-Instance: Params (@sts_ownS) 4.
-Instance: Params (@sts_own) 5.
-Instance: Params (@sts_ctx) 6.
+Instance: Params (@sts_inv) 4 := {}.
+Instance: Params (@sts_ownS) 4 := {}.
+Instance: Params (@sts_own) 5 := {}.
+Instance: Params (@sts_ctx) 6 := {}.
 
 Section sts.
   Context `{invG Σ, stsG Σ sts}.
diff --git a/theories/base_logic/lib/viewshifts.v b/theories/base_logic/lib/viewshifts.v
index e45a87c0c9420662be8df21813459187b458b83d..7443ddc9bf302aac73bb1afcc8052bc56d3bad66 100644
--- a/theories/base_logic/lib/viewshifts.v
+++ b/theories/base_logic/lib/viewshifts.v
@@ -6,7 +6,7 @@ Definition vs `{invG Σ} (E1 E2 : coPset) (P Q : iProp Σ) : iProp Σ :=
   (□ (P -∗ |={E1,E2}=> Q))%I.
 Arguments vs {_ _} _ _ _%I _%I.
 
-Instance: Params (@vs) 4.
+Instance: Params (@vs) 4 := {}.
 Notation "P ={ E1 , E2 }=> Q" := (vs E1 E2 P Q)
   (at level 99, E1,E2 at level 50, Q at level 200,
    format "P  ={ E1 , E2 }=>  Q") : bi_scope.
diff --git a/theories/base_logic/lib/wsat.v b/theories/base_logic/lib/wsat.v
index 3dc30ee425c11f16f50a83022cd33caa6d2820bb..cf629405a33d3d70225970f81ff57c69701cf97a 100644
--- a/theories/base_logic/lib/wsat.v
+++ b/theories/base_logic/lib/wsat.v
@@ -39,18 +39,18 @@ Definition ownI `{invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
   own invariant_name (â—¯ {[ i := invariant_unfold P ]}).
 Arguments ownI {_ _} _ _%I.
 Typeclasses Opaque ownI.
-Instance: Params (@invariant_unfold) 1.
-Instance: Params (@ownI) 3.
+Instance: Params (@invariant_unfold) 1 := {}.
+Instance: Params (@ownI) 3 := {}.
 
 Definition ownE `{invG Σ} (E : coPset) : iProp Σ :=
   own enabled_name (CoPset E).
 Typeclasses Opaque ownE.
-Instance: Params (@ownE) 3.
+Instance: Params (@ownE) 3 := {}.
 
 Definition ownD `{invG Σ} (E : gset positive) : iProp Σ :=
   own disabled_name (GSet E).
 Typeclasses Opaque ownD.
-Instance: Params (@ownD) 3.
+Instance: Params (@ownD) 3 := {}.
 
 Definition wsat `{invG Σ} : iProp Σ :=
   locked (∃ I : gmap positive (iProp Σ),
diff --git a/theories/base_logic/upred.v b/theories/base_logic/upred.v
index c7bb90344f895e3526c9a657321603e3c61e232a..1e14ffb24f22636529acd8094c703c86076742c1 100644
--- a/theories/base_logic/upred.v
+++ b/theories/base_logic/upred.v
@@ -56,7 +56,7 @@ Record uPred (M : ucmraT) : Type := UPred {
 Bind Scope bi_scope with uPred.
 Arguments uPred_holds {_} _%I _ _ : simpl never.
 Add Printing Constructor uPred.
-Instance: Params (@uPred_holds) 3.
+Instance: Params (@uPred_holds) 3 := {}.
 
 Section cofe.
   Context {M : ucmraT}.
diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 62013e901ec1b32a3b6a0fc33e4bcb9aedb54adb..8149b201fcb6daef0dd355f0bb5cf25fed5ff3ec 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -15,7 +15,7 @@ Fixpoint big_sepL2 {PROP : bi} {A B}
   | x1 :: l1, x2 :: l2 => Φ 0 x1 x2 ∗ big_sepL2 (λ n, Φ (S n)) l1 l2
   | _, _ => False
   end%I.
-Instance: Params (@big_sepL2) 3.
+Instance: Params (@big_sepL2) 3 := {}.
 Arguments big_sepL2 {PROP A B} _ !_ !_ /.
 Typeclasses Opaque big_sepL2.
 
diff --git a/theories/bi/derived_connectives.v b/theories/bi/derived_connectives.v
index ec27778846a13e362e0de1df5ad3108be36d690b..d6a12d181b6fafe7aa37d45a4aab5b90d4aeab7b 100644
--- a/theories/bi/derived_connectives.v
+++ b/theories/bi/derived_connectives.v
@@ -3,24 +3,24 @@ From iris.algebra Require Import monoid.
 
 Definition bi_iff {PROP : bi} (P Q : PROP) : PROP := ((P → Q) ∧ (Q → P))%I.
 Arguments bi_iff {_} _%I _%I : simpl never.
-Instance: Params (@bi_iff) 1.
+Instance: Params (@bi_iff) 1 := {}.
 Infix "↔" := bi_iff : bi_scope.
 
 Definition bi_wand_iff {PROP : bi} (P Q : PROP) : PROP :=
   ((P -∗ Q) ∧ (Q -∗ P))%I.
 Arguments bi_wand_iff {_} _%I _%I : simpl never.
-Instance: Params (@bi_wand_iff) 1.
+Instance: Params (@bi_wand_iff) 1 := {}.
 Infix "∗-∗" := bi_wand_iff : bi_scope.
 
 Class Persistent {PROP : bi} (P : PROP) := persistent : P ⊢ <pers> P.
 Arguments Persistent {_} _%I : simpl never.
 Arguments persistent {_} _%I {_}.
 Hint Mode Persistent + ! : typeclass_instances.
-Instance: Params (@Persistent) 1.
+Instance: Params (@Persistent) 1 := {}.
 
 Definition bi_affinely {PROP : bi} (P : PROP) : PROP := (emp ∧ P)%I.
 Arguments bi_affinely {_} _%I : simpl never.
-Instance: Params (@bi_affinely) 1.
+Instance: Params (@bi_affinely) 1 := {}.
 Typeclasses Opaque bi_affinely.
 Notation "'<affine>' P" := (bi_affinely P) : bi_scope.
 
@@ -39,7 +39,7 @@ Hint Mode BiPositive ! : typeclass_instances.
 
 Definition bi_absorbingly {PROP : bi} (P : PROP) : PROP := (True ∗ P)%I.
 Arguments bi_absorbingly {_} _%I : simpl never.
-Instance: Params (@bi_absorbingly) 1.
+Instance: Params (@bi_absorbingly) 1 := {}.
 Typeclasses Opaque bi_absorbingly.
 Notation "'<absorb>' P" := (bi_absorbingly P) : bi_scope.
 
@@ -51,28 +51,28 @@ Hint Mode Absorbing + ! : typeclass_instances.
 Definition bi_persistently_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
   (if p then <pers> P else P)%I.
 Arguments bi_persistently_if {_} !_ _%I /.
-Instance: Params (@bi_persistently_if) 2.
+Instance: Params (@bi_persistently_if) 2 := {}.
 Typeclasses Opaque bi_persistently_if.
 Notation "'<pers>?' p P" := (bi_persistently_if p P) : bi_scope.
 
 Definition bi_affinely_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
   (if p then <affine> P else P)%I.
 Arguments bi_affinely_if {_} !_ _%I /.
-Instance: Params (@bi_affinely_if) 2.
+Instance: Params (@bi_affinely_if) 2 := {}.
 Typeclasses Opaque bi_affinely_if.
 Notation "'<affine>?' p P" := (bi_affinely_if p P) : bi_scope.
 
 Definition bi_intuitionistically {PROP : bi} (P : PROP) : PROP :=
   (<affine> <pers> P)%I.
 Arguments bi_intuitionistically {_} _%I : simpl never.
-Instance: Params (@bi_intuitionistically) 1.
+Instance: Params (@bi_intuitionistically) 1 := {}.
 Typeclasses Opaque bi_intuitionistically.
 Notation "â–¡ P" := (bi_intuitionistically P) : bi_scope.
 
 Definition bi_intuitionistically_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
   (if p then â–¡ P else P)%I.
 Arguments bi_intuitionistically_if {_} !_ _%I /.
-Instance: Params (@bi_intuitionistically_if) 2.
+Instance: Params (@bi_intuitionistically_if) 2 := {}.
 Typeclasses Opaque bi_intuitionistically_if.
 Notation "'â–¡?' p P" := (bi_intuitionistically_if p P) : bi_scope.
 
@@ -82,21 +82,21 @@ Fixpoint sbi_laterN {PROP : sbi} (n : nat) (P : PROP) : PROP :=
   | S n' => â–· sbi_laterN n' P
   end%I.
 Arguments sbi_laterN {_} !_%nat_scope _%I.
-Instance: Params (@sbi_laterN) 2.
+Instance: Params (@sbi_laterN) 2 := {}.
 Notation "â–·^ n P" := (sbi_laterN n P) : bi_scope.
 Notation "â–·? p P" := (sbi_laterN (Nat.b2n p) P) : bi_scope.
 
 Definition sbi_except_0 {PROP : sbi} (P : PROP) : PROP := (▷ False ∨ P)%I.
 Arguments sbi_except_0 {_} _%I : simpl never.
 Notation "â—‡ P" := (sbi_except_0 P) : bi_scope.
-Instance: Params (@sbi_except_0) 1.
+Instance: Params (@sbi_except_0) 1 := {}.
 Typeclasses Opaque sbi_except_0.
 
 Class Timeless {PROP : sbi} (P : PROP) := timeless : ▷ P ⊢ ◇ P.
 Arguments Timeless {_} _%I : simpl never.
 Arguments timeless {_} _%I {_}.
 Hint Mode Timeless + ! : typeclass_instances.
-Instance: Params (@Timeless) 1.
+Instance: Params (@Timeless) 1 := {}.
 
 (** An optional precondition [mP] to [Q].
     TODO: We may actually consider generalizing this to a list of preconditions,
diff --git a/theories/bi/embedding.v b/theories/bi/embedding.v
index 89036d8abc4788a29b016b59e84bd6656667cc30..b5ee8ae509a4ca3ca66f947e13c0b1332dcf7715 100644
--- a/theories/bi/embedding.v
+++ b/theories/bi/embedding.v
@@ -4,7 +4,7 @@ From iris.bi Require Import interface derived_laws_sbi big_op plainly updates.
 Class Embed (A B : Type) := embed : A → B.
 Arguments embed {_ _ _} _%I : simpl never.
 Notation "⎡ P ⎤" := (embed P) : bi_scope.
-Instance: Params (@embed) 3.
+Instance: Params (@embed) 3 := {}.
 Typeclasses Opaque embed.
 
 Hint Mode Embed ! - : typeclass_instances.
diff --git a/theories/bi/interface.v b/theories/bi/interface.v
index 849fd4500a08f928638be15f27beb6077c9e37c6..738ced79e280d16c7f289bc2722a94f55092c740 100644
--- a/theories/bi/interface.v
+++ b/theories/bi/interface.v
@@ -171,17 +171,17 @@ Structure bi := Bi {
 Coercion bi_ofeC (PROP : bi) : ofeT := OfeT PROP (bi_ofe_mixin PROP).
 Canonical Structure bi_ofeC.
 
-Instance: Params (@bi_entails) 1.
-Instance: Params (@bi_emp) 1.
-Instance: Params (@bi_pure) 1.
-Instance: Params (@bi_and) 1.
-Instance: Params (@bi_or) 1.
-Instance: Params (@bi_impl) 1.
-Instance: Params (@bi_forall) 2.
-Instance: Params (@bi_exist) 2.
-Instance: Params (@bi_sep) 1.
-Instance: Params (@bi_wand) 1.
-Instance: Params (@bi_persistently) 1.
+Instance: Params (@bi_entails) 1 := {}.
+Instance: Params (@bi_emp) 1 := {}.
+Instance: Params (@bi_pure) 1 := {}.
+Instance: Params (@bi_and) 1 := {}.
+Instance: Params (@bi_or) 1 := {}.
+Instance: Params (@bi_impl) 1 := {}.
+Instance: Params (@bi_forall) 2 := {}.
+Instance: Params (@bi_exist) 2 := {}.
+Instance: Params (@bi_sep) 1 := {}.
+Instance: Params (@bi_wand) 1 := {}.
+Instance: Params (@bi_persistently) 1 := {}.
 
 Arguments bi_car : simpl never.
 Arguments bi_dist : simpl never.
@@ -224,8 +224,8 @@ Structure sbi := Sbi {
                            sbi_persistently sbi_internal_eq sbi_later;
 }.
 
-Instance: Params (@sbi_later) 1.
-Instance: Params (@sbi_internal_eq) 1.
+Instance: Params (@sbi_later) 1  := {}.
+Instance: Params (@sbi_internal_eq) 1 := {}.
 
 Arguments sbi_later {PROP} _%I : simpl never, rename.
 Arguments sbi_internal_eq {PROP _} _ _ : simpl never, rename.
@@ -256,7 +256,7 @@ Arguments sbi_internal_eq {PROP _} _ _ : simpl never, rename.
 Arguments sbi_later {PROP} _%I : simpl never, rename.
 
 Hint Extern 0 (bi_entails _ _) => reflexivity : core.
-Instance bi_rewrite_relation (PROP : bi) : RewriteRelation (@bi_entails PROP).
+Instance bi_rewrite_relation (PROP : bi) : RewriteRelation (@bi_entails PROP) := {}.
 Instance bi_inhabited {PROP : bi} : Inhabited PROP := populate (bi_pure True).
 
 Notation "P ⊢ Q" := (bi_entails P%I Q%I) : stdpp_scope.
diff --git a/theories/bi/lib/core.v b/theories/bi/lib/core.v
index ce4ab4647a0cb1b2f0f39f36fd67e7f91bfcc4c7..2d737e6554685c4baaa30c7805e27a272d0dc1d9 100644
--- a/theories/bi/lib/core.v
+++ b/theories/bi/lib/core.v
@@ -10,7 +10,7 @@ Definition coreP `{!BiPlainly PROP} (P : PROP) : PROP :=
   (* TODO: Looks like we want notation for affinely-plainly; that lets us avoid
   using conjunction/implication here. *)
   (∀ Q : PROP, <affine> ■ (Q -∗ <pers> Q) -∗ <affine> ■ (P -∗ Q) -∗ Q)%I.
-Instance: Params (@coreP) 1.
+Instance: Params (@coreP) 1 := {}.
 Typeclasses Opaque coreP.
 
 Section core.
diff --git a/theories/bi/monpred.v b/theories/bi/monpred.v
index 2e5e9ed9a51ee3e191b29e839b5dfa84bdcec493..855914c3b4d674c9e711da8011e91b8c6f9a2fde 100644
--- a/theories/bi/monpred.v
+++ b/theories/bi/monpred.v
@@ -357,7 +357,7 @@ Class Objective {I : biIndex} {PROP : bi} (P : monPred I PROP) :=
 Arguments Objective {_ _} _%I.
 Arguments objective_at {_ _} _%I {_}.
 Hint Mode Objective + + ! : typeclass_instances.
-Instance: Params (@Objective) 2.
+Instance: Params (@Objective) 2 := {}.
 
 (** Primitive facts that cannot be deduced from the BI structure. *)
 
diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v
index c52d562f37e14c8150f4a4dc40af45f1e36f53e9..2b35de218db4de6ad572fba8b6b731980127712f 100644
--- a/theories/bi/plainly.v
+++ b/theories/bi/plainly.v
@@ -4,7 +4,7 @@ Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
 
 Class Plainly (A : Type) := plainly : A → A.
 Hint Mode Plainly ! : typeclass_instances.
-Instance: Params (@plainly) 2.
+Instance: Params (@plainly) 2 := {}.
 Notation "â–  P" := (plainly P) : bi_scope.
 
 (* Mixins allow us to create instances easily without having to use Program *)
@@ -87,12 +87,12 @@ Class Plain `{BiPlainly PROP} (P : PROP) := plain : P ⊢ ■ P.
 Arguments Plain {_ _} _%I : simpl never.
 Arguments plain {_ _} _%I {_}.
 Hint Mode Plain + - ! : typeclass_instances.
-Instance: Params (@Plain) 1.
+Instance: Params (@Plain) 1 := {}.
 
 Definition plainly_if `{!BiPlainly PROP} (p : bool) (P : PROP) : PROP :=
   (if p then â–  P else P)%I.
 Arguments plainly_if {_ _} !_ _%I /.
-Instance: Params (@plainly_if) 2.
+Instance: Params (@plainly_if) 2 := {}.
 Typeclasses Opaque plainly_if.
 
 Notation "â– ? p P" := (plainly_if p P) : bi_scope.
diff --git a/theories/bi/tactics.v b/theories/bi/tactics.v
index 8674be92407f9cbb82304ad25451edef2cd4e397..983a5d8d4ef1ccbef431983c414e43863f925c58 100644
--- a/theories/bi/tactics.v
+++ b/theories/bi/tactics.v
@@ -118,17 +118,17 @@ Module bi_reflection. Section bi_reflection.
   Proof. intros. rewrite /= comm. by apply split_l. Qed.
 
   Class Quote (Σ1 Σ2 : list PROP) (P : PROP) (e : expr) := {}.
-  Global Instance quote_True Σ : Quote Σ Σ emp%I EEmp.
+  Global Instance quote_True Σ : Quote Σ Σ emp%I EEmp := {}.
   Global Instance quote_var Σ1 Σ2 P i:
-    rlist.QuoteLookup Σ1 Σ2 P i → Quote Σ1 Σ2 P (EVar i) | 1000.
+    rlist.QuoteLookup Σ1 Σ2 P i → Quote Σ1 Σ2 P (EVar i) | 1000 := {}.
   Global Instance quote_sep Σ1 Σ2 Σ3 P1 P2 e1 e2 :
-    Quote Σ1 Σ2 P1 e1 → Quote Σ2 Σ3 P2 e2 → Quote Σ1 Σ3 (P1 ∗ P2)%I (ESep e1 e2).
+    Quote Σ1 Σ2 P1 e1 → Quote Σ2 Σ3 P2 e2 → Quote Σ1 Σ3 (P1 ∗ P2)%I (ESep e1 e2) := {}.
 
   Class QuoteArgs (Σ : list PROP) (Ps : list PROP) (ns : list nat) := {}.
-  Global Instance quote_args_nil Σ : QuoteArgs Σ nil nil.
+  Global Instance quote_args_nil Σ : QuoteArgs Σ nil nil := {}.
   Global Instance quote_args_cons Σ Ps P ns n :
     rlist.QuoteLookup Σ Σ P n →
-    QuoteArgs Σ Ps ns → QuoteArgs Σ (P :: Ps) (n :: ns).
+    QuoteArgs Σ Ps ns → QuoteArgs Σ (P :: Ps) (n :: ns) := {}.
   End bi_reflection.
 
   Ltac quote :=
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 6dff72c2beda6a0f28233a4e79b7c8ca52e77640..718e153fe7c150e41ed9e9695ef2543b8607da47 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -5,7 +5,7 @@ Import interface.bi derived_laws_bi.bi derived_laws_sbi.bi.
 (* We first define operational type classes for the notations, and then later
 bundle these operational type classes with the laws. *)
 Class BUpd (PROP : Type) : Type := bupd : PROP → PROP.
-Instance : Params (@bupd) 2.
+Instance : Params (@bupd) 2 := {}.
 Hint Mode BUpd ! : typeclass_instances.
 
 Notation "|==> Q" := (bupd Q) : bi_scope.
@@ -13,7 +13,7 @@ Notation "P ==∗ Q" := (P ⊢ |==> Q) (only parsing) : stdpp_scope.
 Notation "P ==∗ Q" := (P -∗ |==> Q)%I : bi_scope.
 
 Class FUpd (PROP : Type) : Type := fupd : coPset → coPset → PROP → PROP.
-Instance: Params (@fupd) 4.
+Instance: Params (@fupd) 4 := {}.
 Hint Mode FUpd ! : typeclass_instances.
 
 Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q) : bi_scope.
diff --git a/theories/bi/weakestpre.v b/theories/bi/weakestpre.v
index d09068871262b71ea6213fcd3bf062e64a60ba92..387b24bf8d789e3f0d09910a85b943dcc9333e24 100644
--- a/theories/bi/weakestpre.v
+++ b/theories/bi/weakestpre.v
@@ -30,12 +30,12 @@ to pick a default value depending on [A]. *)
 Class Wp (Λ : language) (PROP A : Type) :=
   wp : A → coPset → expr Λ → (val Λ → PROP) → PROP.
 Arguments wp {_ _ _ _} _ _ _%E _%I.
-Instance: Params (@wp) 7.
+Instance: Params (@wp) 7 := {}.
 
 Class Twp (Λ : language) (PROP A : Type) :=
   twp : A → coPset → expr Λ → (val Λ → PROP) → PROP.
 Arguments twp {_ _ _ _} _ _ _%E _%I.
-Instance: Params (@twp) 7.
+Instance: Params (@twp) 7 := {}.
 
 (** Notations for partial weakest preconditions *)
 (** Notations without binder -- only parsing because they overlap with the
diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index 3421dccb1b4c07e8edb4010a2fc3f71ba984347f..b6587a44182756f9de2ffe75332f66f89fe29ccf 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -6,7 +6,7 @@ Set Default Proof Using "Type".
 Definition ht `{irisG Λ Σ} (s : stuckness) (E : coPset) (P : iProp Σ)
     (e : expr Λ) (Φ : val Λ → iProp Σ) : iProp Σ :=
   (□ (P -∗ WP e @ s; E {{ Φ }}))%I.
-Instance: Params (@ht) 5.
+Instance: Params (@ht) 5 := {}.
 
 Notation "{{ P } } e @ s ; E {{ Φ } }" := (ht s E P%I e%E Φ%I)
   (at level 20, P, e, Φ at level 200,
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index 545c0ef0f8a5b10480b6db52b6d7d01489b5d042..9e20b1a11c7a888695767c8e4f021644333065de 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -35,7 +35,7 @@ Definition ownP `{ownPG Λ Σ} (σ : state Λ) : iProp Σ :=
   own ownP_name (◯ (Excl' σ)).
 
 Typeclasses Opaque ownP.
-Instance: Params (@ownP) 3.
+Instance: Params (@ownP) 3 := {}.
 
 (* Adequacy *)
 Theorem ownP_adequacy Σ `{ownPPreG Λ Σ} s e σ φ :
diff --git a/theories/proofmode/class_instances_bi.v b/theories/proofmode/class_instances_bi.v
index a73d59f82acc66fac4ed96618bcaa71b21616b50..cc13f1972e98195cd51eb052ae3fb039e91276fc 100644
--- a/theories/proofmode/class_instances_bi.v
+++ b/theories/proofmode/class_instances_bi.v
@@ -998,7 +998,7 @@ Proof. by rewrite /FromForall -embed_forall => <-. Qed.
 
 (** IntoInv *)
 Global Instance into_inv_embed {PROP' : bi} `{BiEmbed PROP PROP'} P N :
-  IntoInv P N → IntoInv ⎡P⎤ N.
+  IntoInv P N → IntoInv ⎡P⎤ N := {}.
 
 (** ElimModal *)
 Global Instance elim_modal_wand φ p p' P P' Q Q' R :
diff --git a/theories/proofmode/environments.v b/theories/proofmode/environments.v
index 562f4a85fed29976f6d4955f476fe34b3b6f5c98..be46ac7c9f88ce63c87129cdf46f6b45e854cc76 100644
--- a/theories/proofmode/environments.v
+++ b/theories/proofmode/environments.v
@@ -10,8 +10,8 @@ Inductive env (A : Type) : Type :=
   | Esnoc : env A → ident → A → env A.
 Arguments Enil {_}.
 Arguments Esnoc {_} _ _ _.
-Instance: Params (@Enil) 1.
-Instance: Params (@Esnoc) 1.
+Instance: Params (@Enil) 1 := {}.
+Instance: Params (@Esnoc) 1 := {}.
 
 Fixpoint env_lookup {A} (i : ident) (Γ : env A) : option A :=
   match Γ with
@@ -37,7 +37,7 @@ Inductive env_wf {A} : env A → Prop :=
 Fixpoint env_to_list {A} (E : env A) : list A :=
   match E with Enil => [] | Esnoc Γ _ x => x :: env_to_list Γ end.
 Coercion env_to_list : env >-> list.
-Instance: Params (@env_to_list) 1.
+Instance: Params (@env_to_list) 1 := {}.
 
 Fixpoint env_dom {A} (Γ : env A) : list ident :=
   match Γ with Enil => [] | Esnoc Γ i _ => i :: env_dom Γ end.
@@ -228,7 +228,7 @@ Record envs_wf {PROP} (Δ : envs PROP) := {
 
 Definition of_envs {PROP} (Δ : envs PROP) : PROP :=
   (⌜envs_wf Δ⌝ ∧ □ [∧] env_intuitionistic Δ ∗ [∗] env_spatial Δ)%I.
-Instance: Params (@of_envs) 1.
+Instance: Params (@of_envs) 1 := {}.
 Arguments of_envs : simpl never.
 
 (* We seal [envs_entails], so that it does not get unfolded by the
@@ -238,7 +238,7 @@ Proof. by eexists. Qed.
 Definition envs_entails := envs_entails_aux.(unseal).
 Definition envs_entails_eq : envs_entails = _ := envs_entails_aux.(seal_eq).
 Arguments envs_entails {PROP} Δ Q%I : rename.
-Instance: Params (@envs_entails) 1.
+Instance: Params (@envs_entails) 1 := {}.
 
 Record envs_Forall2 {PROP : bi} (R : relation PROP) (Δ1 Δ2 : envs PROP) := {
   env_intuitionistic_Forall2 : env_Forall2 R (env_intuitionistic Δ1) (env_intuitionistic Δ2);
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index c33ca55e0423f073497539a880af12b71c870697..21556d314b5151ea6d94cf2ca6c62aea6f46c0a0 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1616,15 +1616,15 @@ Class CopyDestruct {PROP : bi} (P : PROP).
 Arguments CopyDestruct {_} _%I.
 Hint Mode CopyDestruct + ! : typeclass_instances.
 
-Instance copy_destruct_forall {PROP : bi} {A} (Φ : A → PROP) : CopyDestruct (∀ x, Φ x).
+Instance copy_destruct_forall {PROP : bi} {A} (Φ : A → PROP) : CopyDestruct (∀ x, Φ x) := {}.
 Instance copy_destruct_impl {PROP : bi} (P Q : PROP) :
-  CopyDestruct Q → CopyDestruct (P → Q).
+  CopyDestruct Q → CopyDestruct (P → Q) := {}.
 Instance copy_destruct_wand {PROP : bi} (P Q : PROP) :
-  CopyDestruct Q → CopyDestruct (P -∗ Q).
+  CopyDestruct Q → CopyDestruct (P -∗ Q) := {}.
 Instance copy_destruct_affinely {PROP : bi} (P : PROP) :
-  CopyDestruct P → CopyDestruct (<affine> P).
+  CopyDestruct P → CopyDestruct (<affine> P) := {}.
 Instance copy_destruct_persistently {PROP : bi} (P : PROP) :
-  CopyDestruct P → CopyDestruct (<pers> P).
+  CopyDestruct P → CopyDestruct (<pers> P) := {}.
 
 Tactic Notation "iDestructCore" open_constr(lem) "as" constr(p) tactic(tac) :=
   let ident :=