diff --git a/theories/base.v b/theories/base.v
index a0507871fb1bf0f40e62d095ce830f80b11e9e31..9d87f4a6c0b762850bc639fe644fafc78fcd5675 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -114,18 +114,18 @@ Inductive TCOr (P1 P2 : Prop) : Prop :=
   | TCOr_l : P1 → TCOr P1 P2
   | TCOr_r : P2 → TCOr P1 P2.
 Existing Class TCOr.
-Existing Instance TCOr_l | 9.
-Existing Instance TCOr_r | 10.
+Global Existing Instance TCOr_l | 9.
+Global Existing Instance TCOr_r | 10.
 Global Hint Mode TCOr ! ! : typeclass_instances.
 
 Inductive TCAnd (P1 P2 : Prop) : Prop := TCAnd_intro : P1 → P2 → TCAnd P1 P2.
 Existing Class TCAnd.
-Existing Instance TCAnd_intro.
+Global Existing Instance TCAnd_intro.
 Global Hint Mode TCAnd ! ! : typeclass_instances.
 
 Inductive TCTrue : Prop := TCTrue_intro : TCTrue.
 Existing Class TCTrue.
-Existing Instance TCTrue_intro.
+Global Existing Instance TCTrue_intro.
 
 (** The class [TCFalse] is not stricly necessary as one could also use
 [False]. However, users might expect that TCFalse exists and if it
@@ -144,8 +144,8 @@ Inductive TCForall {A} (P : A → Prop) : list A → Prop :=
   | TCForall_nil : TCForall P []
   | TCForall_cons x xs : P x → TCForall P xs → TCForall P (x :: xs).
 Existing Class TCForall.
-Existing Instance TCForall_nil.
-Existing Instance TCForall_cons.
+Global Existing Instance TCForall_nil.
+Global Existing Instance TCForall_cons.
 Global Hint Mode TCForall ! ! ! : typeclass_instances.
 
 (** The class [TCForall2 P l k] is commonly used to transform an input list [l]
@@ -156,8 +156,8 @@ Inductive TCForall2 {A B} (P : A → B → Prop) : list A → list B → Prop :=
   | TCForall2_cons x y xs ys :
      P x y → TCForall2 P xs ys → TCForall2 P (x :: xs) (y :: ys).
 Existing Class TCForall2.
-Existing Instance TCForall2_nil.
-Existing Instance TCForall2_cons.
+Global Existing Instance TCForall2_nil.
+Global Existing Instance TCForall2_cons.
 Global Hint Mode TCForall2 ! ! ! ! - : typeclass_instances.
 Global Hint Mode TCForall2 ! ! ! - ! : typeclass_instances.
 
@@ -165,16 +165,16 @@ Inductive TCExists {A} (P : A → Prop) : list A → Prop :=
   | TCExists_cons_hd x l : P x → TCExists P (x :: l)
   | TCExists_cons_tl x l: TCExists P l → TCExists P (x :: l).
 Existing Class TCExists.
-Existing Instance TCExists_cons_hd | 10.
-Existing Instance TCExists_cons_tl | 20.
+Global Existing Instance TCExists_cons_hd | 10.
+Global Existing Instance TCExists_cons_tl | 20.
 Global Hint Mode TCExists ! ! ! : typeclass_instances.
 
 Inductive TCElemOf {A} (x : A) : list A → Prop :=
   | TCElemOf_here xs : TCElemOf x (x :: xs)
   | TCElemOf_further y xs : TCElemOf x xs → TCElemOf x (y :: xs).
 Existing Class TCElemOf.
-Existing Instance TCElemOf_here.
-Existing Instance TCElemOf_further.
+Global Existing Instance TCElemOf_here.
+Global Existing Instance TCElemOf_further.
 Global Hint Mode TCElemOf ! ! ! : typeclass_instances.
 
 (** We declare both arguments [x] and [y] of [TCEq x y] as outputs, which means
@@ -183,7 +183,7 @@ instance of [TCEq] is [TCEq_refl] below, it can never cause loops. See
 https://gitlab.mpi-sws.org/iris/iris/merge_requests/391 for a use case. *)
 Inductive TCEq {A} (x : A) : A → Prop := TCEq_refl : TCEq x x.
 Existing Class TCEq.
-Existing Instance TCEq_refl.
+Global Existing Instance TCEq_refl.
 Global Hint Mode TCEq ! - - : typeclass_instances.
 
 Lemma TCEq_eq {A} (x1 x2 : A) : TCEq x1 x2 ↔ x1 = x2.
@@ -192,7 +192,7 @@ Proof. split; destruct 1; reflexivity. Qed.
 Inductive TCDiag {A} (C : A → Prop) : A → A → Prop :=
   | TCDiag_diag x : C x → TCDiag C x x.
 Existing Class TCDiag.
-Existing Instance TCDiag_diag.
+Global Existing Instance TCDiag_diag.
 Global Hint Mode TCDiag ! ! ! - : typeclass_instances.
 Global Hint Mode TCDiag ! ! - ! : typeclass_instances.
 
@@ -239,7 +239,7 @@ Notation "X ≠@{ A } Y":= (¬X =@{ A } Y)
 Global Hint Extern 0 (_ = _) => reflexivity : core.
 Global Hint Extern 100 (_ ≠ _) => discriminate : core.
 
-Instance: ∀ A, PreOrder (=@{A}).
+Global Instance: ∀ A, PreOrder (=@{A}).
 Proof. split; repeat intro; congruence. Qed.
 
 (** ** Setoid equality *)
@@ -299,7 +299,7 @@ Definition equivL {A} : Equiv A := (=).
 (** A [Params f n] instance forces the setoid rewriting mechanism not to
 rewrite in the first [n] arguments of the function [f]. We will declare such
 instances for all operational type classes in this development. *)
-Instance: Params (@equiv) 2 := {}.
+Global Instance: Params (@equiv) 2 := {}.
 
 (** The following instance forces [setoid_replace] to use setoid equality
 (for types that have an [Equiv] instance) rather than the standard Leibniz
@@ -459,7 +459,7 @@ Proof. auto. Qed.
 (** The classes [PreOrder], [PartialOrder], and [TotalOrder] use an arbitrary
 relation [R] instead of [⊆] to support multiple orders on the same type. *)
 Definition strict {A} (R : relation A) : relation A := λ X Y, R X Y ∧ ¬R Y X.
-Instance: Params (@strict) 2 := {}.
+Global Instance: Params (@strict) 2 := {}.
 Class PartialOrder {A} (R : relation A) : Prop := {
   partial_order_pre :> PreOrder R;
   partial_order_anti_symm :> AntiSymm (=) R
@@ -630,7 +630,7 @@ Global Instance bool_inhabated : Inhabited bool := populate true.
 Definition bool_le (β1 β2 : bool) : Prop := negb β1 || β2.
 Infix "=.>" := bool_le (at level 70).
 Infix "=.>*" := (Forall2 bool_le) (at level 70).
-Instance: PartialOrder bool_le.
+Global Instance: PartialOrder bool_le.
 Proof. repeat split; repeat intros [|]; compute; tauto. Qed.
 
 Lemma andb_True b1 b2 : b1 && b2 ↔ b1 ∧ b2.
@@ -664,9 +664,9 @@ Notation "(., y )" := (λ x, (x,y)) (only parsing) : stdpp_scope.
 Notation "p .1" := (fst p) (at level 2, left associativity, format "p .1").
 Notation "p .2" := (snd p) (at level 2, left associativity, format "p .2").
 
-Instance: Params (@pair) 2 := {}.
-Instance: Params (@fst) 2 := {}.
-Instance: Params (@snd) 2 := {}.
+Global Instance: Params (@pair) 2 := {}.
+Global Instance: Params (@fst) 2 := {}.
+Global Instance: Params (@snd) 2 := {}.
 
 Notation curry := prod_curry.
 Notation uncurry := prod_uncurry.
@@ -842,7 +842,7 @@ Global Instance empty_inhabited `(Empty A) : Inhabited A := populate ∅.
 
 Class Union A := union: A → A → A.
 Global Hint Mode Union ! : typeclass_instances.
-Instance: Params (@union) 2 := {}.
+Global Instance: Params (@union) 2 := {}.
 Infix "∪" := union (at level 50, left associativity) : stdpp_scope.
 Notation "(∪)" := union (only parsing) : stdpp_scope.
 Notation "( x ∪.)" := (union x) (only parsing) : stdpp_scope.
@@ -856,7 +856,7 @@ Notation "⋃ l" := (union_list l) (at level 20, format "⋃  l") : stdpp_scope.
 
 Class Intersection A := intersection: A → A → A.
 Global Hint Mode Intersection ! : typeclass_instances.
-Instance: Params (@intersection) 2 := {}.
+Global Instance: Params (@intersection) 2 := {}.
 Infix "∩" := intersection (at level 40) : stdpp_scope.
 Notation "(∩)" := intersection (only parsing) : stdpp_scope.
 Notation "( x ∩.)" := (intersection x) (only parsing) : stdpp_scope.
@@ -864,7 +864,7 @@ Notation "(.∩ x )" := (λ y, intersection y x) (only parsing) : stdpp_scope.
 
 Class Difference A := difference: A → A → A.
 Global Hint Mode Difference ! : typeclass_instances.
-Instance: Params (@difference) 2 := {}.
+Global Instance: Params (@difference) 2 := {}.
 Infix "∖" := difference (at level 40, left associativity) : stdpp_scope.
 Notation "(∖)" := difference (only parsing) : stdpp_scope.
 Notation "( x ∖.)" := (difference x) (only parsing) : stdpp_scope.
@@ -874,7 +874,7 @@ Notation "(∖*)" := (zip_with (∖)) (only parsing) : stdpp_scope.
 
 Class Singleton A B := singleton: A → B.
 Global Hint Mode Singleton - ! : typeclass_instances.
-Instance: Params (@singleton) 3 := {}.
+Global Instance: Params (@singleton) 3 := {}.
 Notation "{[ x ]}" := (singleton x) (at level 1) : stdpp_scope.
 Notation "{[ x ; y ; .. ; z ]}" :=
   (union .. (union (singleton x) (singleton y)) .. (singleton z))
@@ -882,7 +882,7 @@ Notation "{[ x ; y ; .. ; z ]}" :=
 
 Class SubsetEq A := subseteq: relation A.
 Global Hint Mode SubsetEq ! : typeclass_instances.
-Instance: Params (@subseteq) 2 := {}.
+Global Instance: Params (@subseteq) 2 := {}.
 Infix "⊆" := subseteq (at level 70) : stdpp_scope.
 Notation "(⊆)" := subseteq (only parsing) : stdpp_scope.
 Notation "( X ⊆.)" := (subseteq X) (only parsing) : stdpp_scope.
@@ -929,7 +929,7 @@ would risk accidentally using [{[ x1; ..; xn ]}] for multisets (leading to
 unexpected results) and lead to ambigious pretty printing for [{[+ x +]}]. *)
 Class DisjUnion A := disj_union: A → A → A.
 Global Hint Mode DisjUnion ! : typeclass_instances.
-Instance: Params (@disj_union) 2 := {}.
+Global Instance: Params (@disj_union) 2 := {}.
 Infix "⊎" := disj_union (at level 50, left associativity) : stdpp_scope.
 Notation "(⊎)" := disj_union (only parsing) : stdpp_scope.
 Notation "( x ⊎.)" := (disj_union x) (only parsing) : stdpp_scope.
@@ -937,7 +937,7 @@ Notation "(.⊎ x )" := (λ y, disj_union y x) (only parsing) : stdpp_scope.
 
 Class SingletonMS A B := singletonMS: A → B.
 Global Hint Mode SingletonMS - ! : typeclass_instances.
-Instance: Params (@singletonMS) 3 := {}.
+Global Instance: Params (@singletonMS) 3 := {}.
 Notation "{[+ x +]}" := (singletonMS x)
   (at level 1, format "{[+  x  +]}") : stdpp_scope.
 Notation "{[+ x ; y ; .. ; z +]}" :=
@@ -959,7 +959,7 @@ Global Hint Mode Lexico ! : typeclass_instances.
 
 Class ElemOf A B := elem_of: A → B → Prop.
 Global Hint Mode ElemOf - ! : typeclass_instances.
-Instance: Params (@elem_of) 3 := {}.
+Global Instance: Params (@elem_of) 3 := {}.
 Infix "∈" := elem_of (at level 70) : stdpp_scope.
 Notation "(∈)" := elem_of (only parsing) : stdpp_scope.
 Notation "( x ∈.)" := (elem_of x) (only parsing) : stdpp_scope.
@@ -977,7 +977,7 @@ Notation "(∉@{ B } )" := (λ x X, x ∉@{B} X) (only parsing) : stdpp_scope.
 
 Class Disjoint A := disjoint : A → A → Prop.
 Global Hint Mode Disjoint ! : typeclass_instances.
-Instance: Params (@disjoint) 2 := {}.
+Global Instance: Params (@disjoint) 2 := {}.
 Infix "##" := disjoint (at level 70) : stdpp_scope.
 Notation "(##)" := disjoint (only parsing) : stdpp_scope.
 Notation "( X ##.)" := (disjoint X) (only parsing) : stdpp_scope.
@@ -1006,19 +1006,19 @@ notations and do not formalize any theory on monads (we do not even define a
 class with the monad laws). *)
 Class MRet (M : Type → Type) := mret: ∀ {A}, A → M A.
 Global Arguments mret {_ _ _} _ : assert.
-Instance: Params (@mret) 3 := {}.
+Global Instance: Params (@mret) 3 := {}.
 Class MBind (M : Type → Type) := mbind : ∀ {A B}, (A → M B) → M A → M B.
 Global Arguments mbind {_ _ _ _} _ !_ / : assert.
-Instance: Params (@mbind) 4 := {}.
+Global Instance: Params (@mbind) 4 := {}.
 Class MJoin (M : Type → Type) := mjoin: ∀ {A}, M (M A) → M A.
 Global Arguments mjoin {_ _ _} !_ / : assert.
-Instance: Params (@mjoin) 3 := {}.
+Global Instance: Params (@mjoin) 3 := {}.
 Class FMap (M : Type → Type) := fmap : ∀ {A B}, (A → B) → M A → M B.
 Global Arguments fmap {_ _ _ _} _ !_ / : assert.
-Instance: Params (@fmap) 4 := {}.
+Global Instance: Params (@fmap) 4 := {}.
 Class OMap (M : Type → Type) := omap: ∀ {A B}, (A → option B) → M A → M B.
 Global Arguments omap {_ _ _ _} _ !_ / : assert.
-Instance: Params (@omap) 4 := {}.
+Global Instance: Params (@omap) 4 := {}.
 
 Notation "m ≫= f" := (mbind f m) (at level 60, right associativity) : stdpp_scope.
 Notation "( m ≫=.)" := (λ f, mbind f m) (only parsing) : stdpp_scope.
@@ -1055,7 +1055,7 @@ on maps. In the file [fin_maps] we will axiomatize finite maps.
 The function look up [m !! k] should yield the element at key [k] in [m]. *)
 Class Lookup (K A M : Type) := lookup: K → M → option A.
 Global Hint Mode Lookup - - ! : typeclass_instances.
-Instance: Params (@lookup) 4 := {}.
+Global Instance: Params (@lookup) 4 := {}.
 Notation "m !! i" := (lookup i m) (at level 20) : stdpp_scope.
 Notation "(!!)" := lookup (only parsing) : stdpp_scope.
 Notation "( m !!.)" := (λ i, m !! i) (only parsing) : stdpp_scope.
@@ -1066,7 +1066,7 @@ Global Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch, assert.
 of the partial [lookup] function. *)
 Class LookupTotal (K A M : Type) := lookup_total : K → M → A.
 Global Hint Mode LookupTotal - - ! : typeclass_instances.
-Instance: Params (@lookup_total) 4 := {}.
+Global Instance: Params (@lookup_total) 4 := {}.
 Notation "m !!! i" := (lookup_total i m) (at level 20) : stdpp_scope.
 Notation "(!!!)" := lookup_total (only parsing) : stdpp_scope.
 Notation "( m !!!.)" := (λ i, m !!! i) (only parsing) : stdpp_scope.
@@ -1076,14 +1076,14 @@ Global Arguments lookup_total _ _ _ _ !_ !_ / : simpl nomatch, assert.
 (** The singleton map *)
 Class SingletonM K A M := singletonM: K → A → M.
 Global Hint Mode SingletonM - - ! : typeclass_instances.
-Instance: Params (@singletonM) 5 := {}.
+Global Instance: Params (@singletonM) 5 := {}.
 Notation "{[ k := a ]}" := (singletonM k a) (at level 1) : stdpp_scope.
 
 (** The function insert [<[k:=a]>m] should update the element at key [k] with
 value [a] in [m]. *)
 Class Insert (K A M : Type) := insert: K → A → M → M.
 Global Hint Mode Insert - - ! : typeclass_instances.
-Instance: Params (@insert) 5 := {}.
+Global Instance: Params (@insert) 5 := {}.
 Notation "<[ k := a ]>" := (insert k a)
   (at level 5, right associativity, format "<[ k := a ]>") : stdpp_scope.
 Global Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch, assert.
@@ -1162,14 +1162,14 @@ Notation "{[ k1 := a1 ; k2 := a2 ; k3 := a3 ; k4 := a4 ; k5 := a5 ; k6 := a6 ; k
 returned. *)
 Class Delete (K M : Type) := delete: K → M → M.
 Global Hint Mode Delete - ! : typeclass_instances.
-Instance: Params (@delete) 4 := {}.
+Global Instance: Params (@delete) 4 := {}.
 Global Arguments delete _ _ _ !_ !_ / : simpl nomatch, assert.
 
 (** The function [alter f k m] should update the value at key [k] using the
 function [f], which is called with the original value. *)
 Class Alter (K A M : Type) := alter: (A → A) → K → M → M.
 Global Hint Mode Alter - - ! : typeclass_instances.
-Instance: Params (@alter) 5 := {}.
+Global Instance: Params (@alter) 5 := {}.
 Global Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch, assert.
 
 (** The function [partial_alter f k m] should update the value at key [k] using the
@@ -1179,14 +1179,14 @@ yields [None]. *)
 Class PartialAlter (K A M : Type) :=
   partial_alter: (option A → option A) → K → M → M.
 Global Hint Mode PartialAlter - - ! : typeclass_instances.
-Instance: Params (@partial_alter) 4 := {}.
+Global Instance: Params (@partial_alter) 4 := {}.
 Global Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
 
 (** The function [dom C m] should yield the domain of [m]. That is a finite
 set of type [C] that contains the keys that are a member of [m]. *)
 Class Dom (M C : Type) := dom: M → C.
 Global Hint Mode Dom ! ! : typeclass_instances.
-Instance: Params (@dom) 3 := {}.
+Global Instance: Params (@dom) 3 := {}.
 Global Arguments dom : clear implicits.
 Global Arguments dom {_} _ {_} !_ / : simpl nomatch, assert.
 
@@ -1195,7 +1195,7 @@ constructing a new map whose value at key [k] is [f (m1 !! k) (m2 !! k)].*)
 Class Merge (M : Type → Type) :=
   merge: ∀ {A B C}, (option A → option B → option C) → M A → M B → M C.
 Global Hint Mode Merge ! : typeclass_instances.
-Instance: Params (@merge) 4 := {}.
+Global Instance: Params (@merge) 4 := {}.
 Global Arguments merge _ _ _ _ _ _ !_ !_ / : simpl nomatch, assert.
 
 (** The function [union_with f m1 m2] is supposed to yield the union of [m1]
@@ -1204,20 +1204,20 @@ both [m1] and [m2]. *)
 Class UnionWith (A M : Type) :=
   union_with: (A → A → option A) → M → M → M.
 Global Hint Mode UnionWith - ! : typeclass_instances.
-Instance: Params (@union_with) 3 := {}.
+Global Instance: Params (@union_with) 3 := {}.
 Global Arguments union_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
 
 (** Similarly for intersection and difference. *)
 Class IntersectionWith (A M : Type) :=
   intersection_with: (A → A → option A) → M → M → M.
 Global Hint Mode IntersectionWith - ! : typeclass_instances.
-Instance: Params (@intersection_with) 3 := {}.
+Global Instance: Params (@intersection_with) 3 := {}.
 Global Arguments intersection_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
 
 Class DifferenceWith (A M : Type) :=
   difference_with: (A → A → option A) → M → M → M.
 Global Hint Mode DifferenceWith - ! : typeclass_instances.
-Instance: Params (@difference_with) 3 := {}.
+Global Instance: Params (@difference_with) 3 := {}.
 Global Arguments difference_with {_ _ _} _ !_ !_ / : simpl nomatch, assert.
 
 Definition intersection_with_list `{IntersectionWith A M}
@@ -1229,7 +1229,7 @@ Global Arguments intersection_with_list _ _ _ _ _ !_ / : assert.
 for the \sqsubseteq symbol. *)
 Class SqSubsetEq A := sqsubseteq: relation A.
 Global Hint Mode SqSubsetEq ! : typeclass_instances.
-Instance: Params (@sqsubseteq) 2 := {}.
+Global Instance: Params (@sqsubseteq) 2 := {}.
 Infix "⊑" := sqsubseteq (at level 70) : stdpp_scope.
 Notation "(⊑)" := sqsubseteq (only parsing) : stdpp_scope.
 Notation "( x ⊑.)" := (sqsubseteq x) (only parsing) : stdpp_scope.
@@ -1244,7 +1244,7 @@ Global Hint Extern 0 (_ ⊑ _) => reflexivity : core.
 
 Class Meet A := meet: A → A → A.
 Global Hint Mode Meet ! : typeclass_instances.
-Instance: Params (@meet) 2 := {}.
+Global Instance: Params (@meet) 2 := {}.
 Infix "⊓" := meet (at level 40) : stdpp_scope.
 Notation "(⊓)" := meet (only parsing) : stdpp_scope.
 Notation "( x ⊓.)" := (meet x) (only parsing) : stdpp_scope.
@@ -1252,7 +1252,7 @@ Notation "(.⊓ y )" := (λ x, meet x y) (only parsing) : stdpp_scope.
 
 Class Join A := join: A → A → A.
 Global Hint Mode Join ! : typeclass_instances.
-Instance: Params (@join) 2 := {}.
+Global Instance: Params (@join) 2 := {}.
 Infix "⊔" := join (at level 50) : stdpp_scope.
 Notation "(⊔)" := join (only parsing) : stdpp_scope.
 Notation "( x ⊔.)" := (join x) (only parsing) : stdpp_scope.
@@ -1301,13 +1301,13 @@ enumerated as a list. These elements, given by the [elements] function, may be
 in any order and should not contain duplicates. *)
 Class Elements A C := elements: C → list A.
 Global Hint Mode Elements - ! : typeclass_instances.
-Instance: Params (@elements) 3 := {}.
+Global Instance: Params (@elements) 3 := {}.
 
 (** We redefine the standard library's [In] and [NoDup] using type classes. *)
 Inductive elem_of_list {A} : ElemOf A (list A) :=
   | elem_of_list_here (x : A) l : x ∈ x :: l
   | elem_of_list_further (x y : A) l : x ∈ l → x ∈ y :: l.
-Existing Instance elem_of_list.
+Global Existing Instance elem_of_list.
 
 Lemma elem_of_list_In {A} (l : list A) x : x ∈ l ↔ In x l.
 Proof.
@@ -1338,7 +1338,7 @@ Class FinSet A C `{ElemOf A C, Empty C, Singleton A C, Union C,
 Class Size C := size: C → nat.
 Global Hint Mode Size ! : typeclass_instances.
 Global Arguments size {_ _} !_ / : simpl nomatch, assert.
-Instance: Params (@size) 2 := {}.
+Global Instance: Params (@size) 2 := {}.
 
 (** The class [MonadSet M] axiomatizes a type constructor [M] that can be
 used to construct a set [M A] with elements of type [A]. The advantage
@@ -1378,7 +1378,7 @@ Instead of instantiating [Infinite] directly, consider using [max_infinite] or
 [inj_infinite] from the [infinite] module. *)
 Class Fresh A C := fresh: C → A.
 Global Hint Mode Fresh - ! : typeclass_instances.
-Instance: Params (@fresh) 3 := {}.
+Global Instance: Params (@fresh) 3 := {}.
 Global Arguments fresh : simpl never.
 
 Class Infinite A := {
diff --git a/theories/binders.v b/theories/binders.v
index 0f0744c66d07f08df8da85a343ca2f12884849fa..1bdd40a0bd27fc2c4ab834e82ea7cf9726da3383 100644
--- a/theories/binders.v
+++ b/theories/binders.v
@@ -77,7 +77,7 @@ Definition binder_delete `{Delete string M} (b : binder) (m : M) : M :=
   match b with BAnon => m | BNamed s => delete s m end.
 Definition binder_insert `{Insert string A M} (b : binder) (x : A) (m : M) : M :=
   match b with BAnon => m | BNamed s => <[s:=x]> m end.
-Instance: Params (@binder_insert) 4 := {}.
+Global Instance: Params (@binder_insert) 4 := {}.
 
 Section binder_delete_insert.
   Context `{FinMap string M}.
diff --git a/theories/countable.v b/theories/countable.v
index b1cbe454c39107fb48be4e6427eb15644b616119..c4481ba495cfb74b57e5d1d9a9d4280866198c44 100644
--- a/theories/countable.v
+++ b/theories/countable.v
@@ -111,24 +111,24 @@ Section inj_countable'.
 End inj_countable'.
 
 (** ** Empty *)
-Program Instance Empty_set_countable : Countable Empty_set :=
+Global Program Instance Empty_set_countable : Countable Empty_set :=
   {| encode u := 1; decode p := None |}.
 Next Obligation. by intros []. Qed.
 
 (** ** Unit *)
-Program Instance unit_countable : Countable unit :=
+Global Program Instance unit_countable : Countable unit :=
   {| encode u := 1; decode p := Some () |}.
 Next Obligation. by intros []. Qed.
 
 (** ** Bool *)
-Program Instance bool_countable : Countable bool := {|
+Global Program Instance bool_countable : Countable bool := {|
   encode b := if b then 1 else 2;
   decode p := Some match p return bool with 1 => true | _ => false end
 |}.
 Next Obligation. by intros []. Qed.
 
 (** ** Option *)
-Program Instance option_countable `{Countable A} : Countable (option A) := {|
+Global Program Instance option_countable `{Countable A} : Countable (option A) := {|
   encode o := match o with None => 1 | Some x => Pos.succ (encode x) end;
   decode p := if decide (p = 1) then Some None else Some <$> decode (Pos.pred p)
 |}.
@@ -138,7 +138,7 @@ Next Obligation.
 Qed.
 
 (** ** Sums *)
-Program Instance sum_countable `{Countable A} `{Countable B} :
+Global Program Instance sum_countable `{Countable A} `{Countable B} :
   Countable (A + B)%type := {|
     encode xy :=
       match xy with inl x => (encode x)~0 | inr y => (encode y)~1 end;
@@ -211,7 +211,7 @@ Proof.
   { intros p'. by induction p'; simplify_option_eq. }
   revert q. by induction p; intros [?|?|]; simplify_option_eq.
 Qed.
-Program Instance prod_countable `{Countable A} `{Countable B} :
+Global Program Instance prod_countable `{Countable A} `{Countable B} :
   Countable (A * B)%type := {|
     encode xy := prod_encode (encode (xy.1)) (encode (xy.2));
     decode p :=
@@ -240,7 +240,7 @@ Qed.
 (** ** Numbers *)
 Global Instance pos_countable : Countable positive :=
   {| encode := id; decode := Some; decode_encode x := eq_refl |}.
-Program Instance N_countable : Countable N := {|
+Global Program Instance N_countable : Countable N := {|
   encode x := match x with N0 => 1 | Npos p => Pos.succ p end;
   decode p := if decide (p = 1) then Some 0%N else Some (Npos (Pos.pred p))
 |}.
@@ -248,18 +248,18 @@ Next Obligation.
   intros [|p]; simpl; [done|].
   by rewrite decide_False, Pos.pred_succ by (by destruct p).
 Qed.
-Program Instance Z_countable : Countable Z := {|
+Global Program Instance Z_countable : Countable Z := {|
   encode x := match x with Z0 => 1 | Zpos p => p~0 | Zneg p => p~1 end;
   decode p := Some match p with 1 => Z0 | p~0 => Zpos p | p~1 => Zneg p end
 |}.
 Next Obligation. by intros [|p|p]. Qed.
-Program Instance nat_countable : Countable nat :=
+Global Program Instance nat_countable : Countable nat :=
   {| encode x := encode (N.of_nat x); decode p := N.to_nat <$> decode p |}.
 Next Obligation.
   by intros x; lazy beta; rewrite decode_encode; csimpl; rewrite Nat2N.id.
 Qed.
 
-Program Instance Qc_countable : Countable Qc :=
+Global Program Instance Qc_countable : Countable Qc :=
   inj_countable
     (λ p : Qc, let 'Qcmake (x # y) _ := p return _ in (x,y))
     (λ q : Z * positive, let '(x,y) := q return _ in Some (Q2Qc (x # y))) _.
@@ -267,7 +267,7 @@ Next Obligation.
   intros [[x y] Hcan]. f_equal. apply Qc_is_canon. simpl. by rewrite Hcan.
 Qed.
 
-Program Instance Qp_countable : Countable Qp :=
+Global Program Instance Qp_countable : Countable Qp :=
   inj_countable
     Qp_to_Qc
     (λ p : Qc, guard (0 < p)%Qc as Hp; Some (mk_Qp p Hp)) _.
@@ -276,7 +276,7 @@ Next Obligation.
   case_match; [|done]. f_equal. by apply Qp_to_Qc_inj_iff.
 Qed.
 
-Program Instance fin_countable n : Countable (fin n) :=
+Global Program Instance fin_countable n : Countable (fin n) :=
   inj_countable
     fin_to_nat
     (λ m : nat, guard (m < n)%nat as Hm; Some (nat_to_fin Hm)) _.
@@ -334,7 +334,7 @@ Proof.
       by (by rewrite reverse_length).
 Qed.
 
-Program Instance gen_tree_countable `{Countable T} : Countable (gen_tree T) :=
+Global Program Instance gen_tree_countable `{Countable T} : Countable (gen_tree T) :=
   inj_countable gen_tree_to_list (gen_tree_of_list []) _.
 Next Obligation.
   intros T ?? t.
@@ -342,7 +342,7 @@ Next Obligation.
 Qed.
 
 (** ** Sigma *)
-Program Instance countable_sig `{Countable A} (P : A → Prop)
+Global Program Instance countable_sig `{Countable A} (P : A → Prop)
         `{!∀ x, Decision (P x), !∀ x, ProofIrrel (P x)} :
   Countable { x : A | P x } :=
   inj_countable proj1_sig (λ x, guard (P x) as Hx; Some (x ↾ Hx)) _.
diff --git a/theories/decidable.v b/theories/decidable.v
index 64befc94428f4fb0060c141dc32668b2ba27f6ad..e5572fe50daed3a0ae30a76e7bf1dfe3a12c3c49 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -12,7 +12,7 @@ Proof. firstorder. Qed.
 
 Lemma Is_true_reflect (b : bool) : reflect b b.
 Proof. destruct b; [left; constructor | right; intros []]. Qed.
-Instance: Inj (=) (↔) Is_true.
+Global Instance: Inj (=) (↔) Is_true.
 Proof. intros [] []; simpl; intuition. Qed.
 
 Lemma decide_True {A} `{Decision P} (x y : A) :
diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index 3b856ab52d928ea044fff0b68e7c26191b2a6300..21b71cc63eb923230b0ba956f20b074476529bbf 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -36,7 +36,7 @@ Fixpoint fresh_list `{Fresh A C, Union C, Singleton A C}
   | 0 => []
   | S n => let x := fresh X in x :: fresh_list n ({[ x ]} ∪ X)
   end.
-Instance: Params (@fresh_list) 6 := {}.
+Global Instance: Params (@fresh_list) 6 := {}.
 
 (** The following inductive predicate classifies that a list of elements is
 in fact fresh w.r.t. a set [X]. *)
diff --git a/theories/finite.v b/theories/finite.v
index 9e58dcd6af54cfe9353255ea45e2a1f3d1d25520..0e9e6fbb005c2bd4ec43a63c39ab2ded80c78330 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -242,7 +242,7 @@ Section bijective_finite.
     surjective_finite f.
 End bijective_finite.
 
-Program Instance option_finite `{Finite A} : Finite (option A) :=
+Global Program Instance option_finite `{Finite A} : Finite (option A) :=
   {| enum := None :: (Some <$> enum A) |}.
 Next Obligation.
   constructor.
@@ -256,19 +256,19 @@ Qed.
 Lemma option_cardinality `{Finite A} : card (option A) = S (card A).
 Proof. unfold card. simpl. by rewrite fmap_length. Qed.
 
-Program Instance Empty_set_finite : Finite Empty_set := {| enum := [] |}.
+Global Program Instance Empty_set_finite : Finite Empty_set := {| enum := [] |}.
 Next Obligation. by apply NoDup_nil. Qed.
 Next Obligation. intros []. Qed.
 Lemma Empty_set_card : card Empty_set = 0.
 Proof. done. Qed.
 
-Program Instance unit_finite : Finite () := {| enum := [tt] |}.
+Global Program Instance unit_finite : Finite () := {| enum := [tt] |}.
 Next Obligation. apply NoDup_singleton. Qed.
 Next Obligation. intros []. by apply elem_of_list_singleton. Qed.
 Lemma unit_card : card unit = 1.
 Proof. done. Qed.
 
-Program Instance bool_finite : Finite bool := {| enum := [true; false] |}.
+Global Program Instance bool_finite : Finite bool := {| enum := [true; false] |}.
 Next Obligation.
   constructor; [ by rewrite elem_of_list_singleton | apply NoDup_singleton ].
 Qed.
@@ -276,7 +276,7 @@ Next Obligation. intros [|]; [ left | right; left ]. Qed.
 Lemma bool_card : card bool = 2.
 Proof. done. Qed.
 
-Program Instance sum_finite `{Finite A, Finite B} : Finite (A + B)%type :=
+Global Program Instance sum_finite `{Finite A, Finite B} : Finite (A + B)%type :=
   {| enum := (inl <$> enum A) ++ (inr <$> enum B) |}.
 Next Obligation.
   intros. apply NoDup_app; split_and?.
@@ -291,7 +291,7 @@ Qed.
 Lemma sum_card `{Finite A, Finite B} : card (A + B) = card A + card B.
 Proof. unfold card. simpl. by rewrite app_length, !fmap_length. Qed.
 
-Program Instance prod_finite `{Finite A, Finite B} : Finite (A * B)%type :=
+Global Program Instance prod_finite `{Finite A, Finite B} : Finite (A * B)%type :=
   {| enum := foldr (λ x, (pair x <$> enum B ++.)) [] (enum A) |}.
 Next Obligation.
   intros A ?????. induction (NoDup_enum A) as [|x xs Hx Hxs IH]; simpl.
@@ -325,7 +325,7 @@ Definition list_enum {A} (l : list A) : ∀ n, list { l : list A | length l = n
   | S n => foldr (λ x, (sig_map (x ::.) (λ _ H, f_equal S H) <$> (go n) ++.)) [] l
   end.
 
-Program Instance list_finite `{Finite A} n : Finite { l : list A | length l = n } :=
+Global Program Instance list_finite `{Finite A} n : Finite { l : list A | length l = n } :=
   {| enum := list_enum (enum A) n |}.
 Next Obligation.
   intros A ?? n. induction n as [|n IH]; simpl; [apply NoDup_singleton |].
@@ -361,7 +361,7 @@ Qed.
 
 Fixpoint fin_enum (n : nat) : list (fin n) :=
   match n with 0 => [] | S n => 0%fin :: (FS <$> fin_enum n) end.
-Program Instance fin_finite n : Finite (fin n) := {| enum := fin_enum n |}.
+Global Program Instance fin_finite n : Finite (fin n) := {| enum := fin_enum n |}.
 Next Obligation.
   intros n. induction n; simpl; constructor.
   - rewrite elem_of_list_fmap. by intros (?&?&?).
diff --git a/theories/gmap.v b/theories/gmap.v
index f8ab424c85df15cf78e216f84381518d85c2d4d3..944fd3f622a635e4d24c579b8a4688d25402e8a9 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -134,7 +134,7 @@ Proof.
     by rewrite lookup_merge by done; destruct (m1 !! _), (m2 !! _).
 Qed.
 
-Program Instance gmap_countable
+Global Program Instance gmap_countable
     `{Countable K, Countable A} : Countable (gmap K A) := {
   encode m := encode (map_to_list m : list (K * A));
   decode p := list_to_map <$> decode p
diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index 311ded6ec5cc15e8b197cc63e52d2158964a1e37..2516dc08e78733766c3a090a5c11f940f58da3c9 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -9,7 +9,7 @@ Global Arguments gmultiset_car {_ _ _} _ : assert.
 Global Instance gmultiset_eq_dec `{Countable A} : EqDecision (gmultiset A).
 Proof. solve_decision. Defined.
 
-Program Instance gmultiset_countable `{Countable A} :
+Global Program Instance gmultiset_countable `{Countable A} :
     Countable (gmultiset A) := {|
   encode X := encode (gmultiset_car X); decode p := GMultiSet <$> decode p
 |}.
diff --git a/theories/infinite.v b/theories/infinite.v
index 395756c0dd776e14153b0bea276e9b18bc56933e..99c4936eeaa25b9a91e0788b9c4aa2b21ffba62c 100644
--- a/theories/infinite.v
+++ b/theories/infinite.v
@@ -106,19 +106,19 @@ Section max_infinite.
 End max_infinite.
 
 (** Instances for number types *)
-Program Instance nat_infinite : Infinite nat :=
+Global Program Instance nat_infinite : Infinite nat :=
   max_infinite (Nat.max ∘ S) 0 (<) _ _ _ _.
 Solve Obligations with (intros; simpl; lia).
 
-Program Instance N_infinite : Infinite N :=
+Global Program Instance N_infinite : Infinite N :=
   max_infinite (N.max ∘ N.succ) 0%N N.lt _ _ _ _.
 Solve Obligations with (intros; simpl; lia).
 
-Program Instance positive_infinite : Infinite positive :=
+Global Program Instance positive_infinite : Infinite positive :=
   max_infinite (Pos.max ∘ Pos.succ) 1%positive Pos.lt _ _ _ _.
 Solve Obligations with (intros; simpl; lia).
 
-Program Instance Z_infinite: Infinite Z :=
+Global Program Instance Z_infinite: Infinite Z :=
   max_infinite (Z.max ∘ Z.succ) 0%Z Z.lt _ _ _ _.
 Solve Obligations with (intros; simpl; lia).
 
@@ -137,7 +137,7 @@ Global Instance prod_infinite_r `{Inhabited A, Infinite B} : Infinite (A * B) :=
   inj_infinite (inhabitant ,.) (Some ∘ snd) (λ _, eq_refl).
 
 (** Instance for lists *)
-Program Instance list_infinite `{Inhabited A} : Infinite (list A) := {|
+Global Program Instance list_infinite `{Inhabited A} : Infinite (list A) := {|
   infinite_fresh xxs := replicate (fresh (length <$> xxs)) inhabitant
 |}.
 Next Obligation.
@@ -148,5 +148,5 @@ Qed.
 Next Obligation. unfold fresh. by intros A ? xs1 xs2 ->. Qed.
 
 (** Instance for strings *)
-Program Instance string_infinite : Infinite string :=
+Global Program Instance string_infinite : Infinite string :=
   search_infinite pretty.
diff --git a/theories/list.v b/theories/list.v
index e5127a299b179582d5d53ee08d5732b109bb8131..9bd281c5f92d9ad67317b711a7646acd9f31de32 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -11,9 +11,9 @@ Global Arguments length {_} _ : assert.
 Global Arguments cons {_} _ _ : assert.
 Global Arguments app {_} _ _ : assert.
 
-Instance: Params (@length) 1 := {}.
-Instance: Params (@cons) 1 := {}.
-Instance: Params (@app) 1 := {}.
+Global Instance: Params (@length) 1 := {}.
+Global Instance: Params (@cons) 1 := {}.
+Global Instance: Params (@app) 1 := {}.
 
 Notation tail := tl.
 Notation take := firstn.
@@ -24,10 +24,10 @@ Global Arguments tail {_} _ : assert.
 Global Arguments take {_} !_ !_ / : assert.
 Global Arguments drop {_} !_ !_ / : assert.
 
-Instance: Params (@head) 1 := {}.
-Instance: Params (@tail) 1 := {}.
-Instance: Params (@take) 1 := {}.
-Instance: Params (@drop) 1 := {}.
+Global Instance: Params (@head) 1 := {}.
+Global Instance: Params (@tail) 1 := {}.
+Global Instance: Params (@take) 1 := {}.
+Global Instance: Params (@drop) 1 := {}.
 
 Global Arguments Permutation {_} _ _ : assert.
 Global Arguments Forall_cons {_} _ _ _ _ _ : assert.
@@ -61,7 +61,7 @@ Global Instance maybe_cons {A} : Maybe2 (@cons A) := λ l,
 Inductive list_equiv `{Equiv A} : Equiv (list A) :=
   | nil_equiv : [] ≡ []
   | cons_equiv x y l k : x ≡ y → l ≡ k → x :: l ≡ y :: k.
-Existing Instance list_equiv.
+Global Existing Instance list_equiv.
 
 (** The operation [l !! i] gives the [i]th element of the list [l], or [None]
 in case [i] is out of bounds. *)
@@ -102,7 +102,7 @@ Fixpoint list_inserts {A} (i : nat) (k l : list A) : list A :=
   | [] => l
   | y :: k => <[i:=y]>(list_inserts (S i) k l)
   end.
-Instance: Params (@list_inserts) 1 := {}.
+Global Instance: Params (@list_inserts) 1 := {}.
 
 (** The operation [delete i l] removes the [i]th element of [l] and moves
 all consecutive elements one position ahead. In case [i] is out of bounds,
@@ -117,7 +117,7 @@ Global Instance list_delete {A} : Delete nat (list A) :=
 (** The function [option_list o] converts an element [Some x] into the
 singleton list [[x]], and [None] into the empty list [[]]. *)
 Definition option_list {A} : option A → list A := option_rect _ (λ x, [x]) [].
-Instance: Params (@option_list) 1 := {}.
+Global Instance: Params (@option_list) 1 := {}.
 Global Instance maybe_list_singleton {A} : Maybe (λ x : A, [x]) := λ l,
   match l with [x] => Some x | _ => None end.
 
@@ -138,37 +138,37 @@ Definition list_find {A} P `{∀ x, Decision (P x)} : list A → option (nat * A
   | [] => None
   | x :: l => if decide (P x) then Some (0,x) else prod_map S id <$> go l
   end.
-Instance: Params (@list_find) 3 := {}.
+Global Instance: Params (@list_find) 3 := {}.
 
 (** The function [replicate n x] generates a list with length [n] of elements
 with value [x]. *)
 Fixpoint replicate {A} (n : nat) (x : A) : list A :=
   match n with 0 => [] | S n => x :: replicate n x end.
-Instance: Params (@replicate) 2 := {}.
+Global Instance: Params (@replicate) 2 := {}.
 
 (** The function [rotate n l] rotates the list [l] by [n], e.g., [rotate 1
 [x0; x1; ...; xm]] becomes [x1; ...; xm; x0]. Rotating by a multiple of
 [length l] is the identity function. **)
 Definition rotate {A} (n : nat) (l : list A) : list A :=
   drop (n `mod` length l) l ++ take (n `mod` length l) l.
-Instance: Params (@rotate) 2 := {}.
+Global Instance: Params (@rotate) 2 := {}.
 
 (** The function [rotate_take s e l] returns the range between the
 indices [s] (inclusive) and [e] (exclusive) of [l]. If [e ≤ s], all
 elements after [s] and before [e] are returned. *)
 Definition rotate_take {A} (s e : nat) (l : list A) : list A :=
   take (rotate_nat_sub s e (length l)) (rotate s l).
-Instance: Params (@rotate_take) 3 := {}.
+Global Instance: Params (@rotate_take) 3 := {}.
 
 (** The function [reverse l] returns the elements of [l] in reverse order. *)
 Definition reverse {A} (l : list A) : list A := rev_append l [].
-Instance: Params (@reverse) 1 := {}.
+Global Instance: Params (@reverse) 1 := {}.
 
 (** The function [last l] returns the last element of the list [l], or [None]
 if the list [l] is empty. *)
 Fixpoint last {A} (l : list A) : option A :=
   match l with [] => None | [x] => Some x | _ :: l => last l end.
-Instance: Params (@last) 1 := {}.
+Global Instance: Params (@last) 1 := {}.
 
 (** The function [resize n y l] takes the first [n] elements of [l] in case
 [length l ≤ n], and otherwise appends elements with value [x] to [l] to obtain
@@ -179,7 +179,7 @@ Fixpoint resize {A} (n : nat) (y : A) (l : list A) : list A :=
   | x :: l => match n with 0 => [] | S n => x :: resize n y l end
   end.
 Global Arguments resize {_} !_ _ !_ : assert.
-Instance: Params (@resize) 2 := {}.
+Global Instance: Params (@resize) 2 := {}.
 
 (** The function [reshape k l] transforms [l] into a list of lists whose sizes
 are specified by [k]. In case [l] is too short, the resulting list will be
@@ -188,7 +188,7 @@ Fixpoint reshape {A} (szs : list nat) (l : list A) : list (list A) :=
   match szs with
   | [] => [] | sz :: szs => take sz l :: reshape szs (drop sz l)
   end.
-Instance: Params (@reshape) 2 := {}.
+Global Instance: Params (@reshape) 2 := {}.
 
 Definition sublist_lookup {A} (i n : nat) (l : list A) : option (list A) :=
   guard (i + n ≤ length l); Some (take n (drop i l)).
diff --git a/theories/nat_cancel.v b/theories/nat_cancel.v
index b6cc0ae8f3ece77be94676b1763ef5b95eb3d7c1..d0372a22a20fe297667b11cbfc008f3ede198dee 100644
--- a/theories/nat_cancel.v
+++ b/theories/nat_cancel.v
@@ -45,7 +45,7 @@ Module nat_cancel.
   Global Hint Mode NatCancelL ! ! - - : typeclass_instances.
   Class NatCancelR (m n m' n' : nat) := nat_cancel_r : NatCancelL m n m' n'.
   Global Hint Mode NatCancelR ! ! - - : typeclass_instances.
-  Existing Instance nat_cancel_r | 100.
+  Global Existing Instance nat_cancel_r | 100.
 
   (** The implementation of the canceler is highly non-deterministic, but since
   it will always succeed, no backtracking will ever be performed. In order to
diff --git a/theories/natmap.v b/theories/natmap.v
index 0589e1017eef9ab19b2af98ee2d889e27922caaa..3da7907027c217685ec68ff72e14e669d50767ea 100644
--- a/theories/natmap.v
+++ b/theories/natmap.v
@@ -205,7 +205,7 @@ Qed.
 Global Instance natmap_map: FMap natmap := λ A B f m,
   let (l,Hl) := m in NatMap (natmap_map_raw f l) (natmap_map_wf _ _ Hl).
 
-Instance: FinMap nat natmap.
+Global Instance: FinMap nat natmap.
 Proof.
   split.
   - unfold lookup, natmap_lookup. intros A [l1 Hl1] [l2 Hl2] E.
@@ -257,7 +257,7 @@ Qed.
 (** Finally, we can construct sets of [nat]s satisfying extensional equality. *)
 Notation natset := (mapset natmap).
 Global Instance natmap_dom {A} : Dom (natmap A) natset := mapset_dom.
-Instance: FinMapDom nat natmap natset := mapset_dom_spec.
+Global Instance: FinMapDom nat natmap natset := mapset_dom_spec.
 
 (* Fixpoint avoids this definition from being unfolded *)
 Definition bools_to_natset (βs : list bool) : natset :=
diff --git a/theories/nmap.v b/theories/nmap.v
index 6010831824eef396b23622291c4bb36058db7fea..2e1916d89780b8ffc47ec9be5d91313725517339 100644
--- a/theories/nmap.v
+++ b/theories/nmap.v
@@ -44,7 +44,7 @@ Global Instance Nmerge: Merge Nmap := λ A B C f t1 t2,
 Global Instance Nfmap: FMap Nmap := λ A B f t,
   match t with NMap o t => NMap (f <$> o) (f <$> t) end.
 
-Instance: FinMap N Nmap.
+Global Instance: FinMap N Nmap.
 Proof.
   split.
   - intros ? [??] [??] H. f_equal; [apply (H 0)|].
@@ -81,4 +81,4 @@ Qed.
 (** We construct sets of [N]s satisfying extensional equality. *)
 Notation Nset := (mapset Nmap).
 Global Instance Nmap_dom {A} : Dom (Nmap A) Nset := mapset_dom.
-Instance: FinMapDom N Nmap Nset := mapset_dom_spec.
+Global Instance: FinMapDom N Nmap Nset := mapset_dom_spec.
diff --git a/theories/numbers.v b/theories/numbers.v
index f3563fb485bacea9861683df2a1fbe9674db70bd..b17f5efb18ce7dba0ff671ef7582f32ffc180318 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -84,7 +84,7 @@ Global Instance Nat_divide_dec : RelDecision Nat.divide.
 Proof.
   refine (λ x y, cast_if (decide (lcm x y = y))); by rewrite Nat.divide_lcm_iff.
 Defined.
-Instance: PartialOrder divide.
+Global Instance: PartialOrder divide.
 Proof.
   repeat split; try apply _. intros ??. apply Nat.divide_antisym_nonneg; lia.
 Qed.
@@ -302,10 +302,10 @@ Global Instance Npos_inj : Inj (=) (=) Npos.
 Proof. by injection 1. Qed.
 
 Global Instance N_eq_dec: EqDecision N := N.eq_dec.
-Program Instance N_le_dec : RelDecision N.le := λ x y,
+Global Program Instance N_le_dec : RelDecision N.le := λ x y,
   match N.compare x y with Gt => right _ | _ => left _ end.
 Solve Obligations with naive_solver.
-Program Instance N_lt_dec : RelDecision N.lt := λ x y,
+Global Program Instance N_lt_dec : RelDecision N.lt := λ x y,
   match N.compare x y with Lt => left _ | _ => right _ end.
 Solve Obligations with naive_solver.
 Global Instance N_inhabited: Inhabited N := populate 1%N.
@@ -573,11 +573,11 @@ Proof. apply Qred_identity; auto using Z.gcd_1_r. Qed.
 Definition Qc_of_Z (n : Z) : Qc := Qcmake _ (inject_Z_Qred n).
 
 Global Instance Qc_eq_dec: EqDecision Qc := Qc_eq_dec.
-Program Instance Qc_le_dec: RelDecision Qcle := λ x y,
+Global Program Instance Qc_le_dec: RelDecision Qcle := λ x y,
   if Qclt_le_dec y x then right _ else left _.
 Next Obligation. intros x y; apply Qclt_not_le. Qed.
 Next Obligation. done. Qed.
-Program Instance Qc_lt_dec: RelDecision Qclt := λ x y,
+Global Program Instance Qc_lt_dec: RelDecision Qclt := λ x y,
   if Qclt_le_dec x y then left _ else right _.
 Next Obligation. done. Qed.
 Next Obligation. intros x y; apply Qcle_not_lt. Qed.
diff --git a/theories/option.v b/theories/option.v
index 7c10bc438c4a1eaaa0c32921b30249edb215605c..8ca6196886f812c19750db73bf99e0e03a92e0eb 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -21,7 +21,7 @@ Proof. congruence. Qed.
 (** The [from_option] is the eliminator for option. *)
 Definition from_option {A B} (f : A → B) (y : B) (mx : option A) : B :=
   match mx with None => y | Some x => f x end.
-Instance: Params (@from_option) 3 := {}.
+Global Instance: Params (@from_option) 3 := {}.
 Global Arguments from_option {_ _} _ _ !_ / : assert.
 
 (** The eliminator with the identity function. *)
@@ -38,7 +38,7 @@ Lemma option_eq_1_alt {A} (mx my : option A) x :
 Proof. congruence. Qed.
 
 Definition is_Some {A} (mx : option A) := ∃ x, mx = Some x.
-Instance: Params (@is_Some) 1 := {}.
+Global Instance: Params (@is_Some) 1 := {}.
 
 Lemma is_Some_alt {A} (mx : option A) :
   is_Some mx ↔ match mx with Some _ => True | None => False end.
diff --git a/theories/pmap.v b/theories/pmap.v
index a6630209f4f0fbb206be0acdc9e065fd107e5cad..f62d6c6c2f393df8d48f9296065436db54edf7a2 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -302,7 +302,7 @@ Proof.
   - intros ??? ?? [??] [??] ?. by apply Pmerge_lookup.
 Qed.
 
-Program Instance Pmap_countable `{Countable A} : Countable (Pmap A) := {
+Global Program Instance Pmap_countable `{Countable A} : Countable (Pmap A) := {
   encode m := encode (map_to_list m : list (positive * A));
   decode p := list_to_map <$> decode p
 }.
diff --git a/theories/sets.v b/theories/sets.v
index 984e667cae0d3711fc0c55bfed32df08ee6c2e4b..12d584db2de21078e7864a023195e19cf0f76369 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -1242,7 +1242,7 @@ End set_seq.
 (** Mimimal elements *)
 Definition minimal `{ElemOf A C} (R : relation A) (x : A) (X : C) : Prop :=
   ∀ y, y ∈ X → R y x → R x y.
-Instance: Params (@minimal) 5 := {}.
+Global Instance: Params (@minimal) 5 := {}.
 Typeclasses Opaque minimal.
 
 Section minimal.
diff --git a/theories/strings.v b/theories/strings.v
index 5cf255a6d3959dd1aeb39cb11c30e8acaf76106b..051c42925e821fdb74742135bd39a32f42954f0e 100644
--- a/theories/strings.v
+++ b/theories/strings.v
@@ -111,7 +111,7 @@ Lemma string_of_to_pos s : string_of_pos (string_to_pos s) = s.
 Proof.
   unfold string_of_pos. by induction s as [|[[][][][][][][][]]]; f_equal/=.
 Qed.
-Program Instance string_countable : Countable string := {|
+Global Program Instance string_countable : Countable string := {|
   encode := string_to_pos; decode p := Some (string_of_pos p)
 |}.
 Solve Obligations with naive_solver eauto using string_of_to_pos with f_equal.
diff --git a/theories/zmap.v b/theories/zmap.v
index e53aeb74bdccb9d9df8d47338783ef78fba2c163..32e1ed3c7a93380825cb7b579d87d0975fae488f 100644
--- a/theories/zmap.v
+++ b/theories/zmap.v
@@ -47,7 +47,7 @@ Global Instance Zmerge: Merge Zmap := λ A B C f t1 t2,
 Global Instance Nfmap: FMap Zmap := λ A B f t,
   match t with ZMap o t t' => ZMap (f <$> o) (f <$> t) (f <$> t') end.
 
-Instance: FinMap Z Zmap.
+Global Instance: FinMap Z Zmap.
 Proof.
   split.
   - intros ? [??] [??] H. f_equal.
@@ -92,4 +92,4 @@ Qed.
 (** We construct sets of [Z]s satisfying extensional equality. *)
 Notation Zset := (mapset Zmap).
 Global Instance Zmap_dom {A} : Dom (Zmap A) Zset := mapset_dom.
-Instance: FinMapDom Z Zmap Zset := mapset_dom_spec.
+Global Instance: FinMapDom Z Zmap Zset := mapset_dom_spec.