From 68447aa2dcad3f1a8d4e74f31d061f1a303630d8 Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jihgfee@gmail.com>
Date: Tue, 29 Jun 2021 13:39:36 +0200
Subject: [PATCH] Added "Global" instance locality to resolve future Coq
 warnings

---
 theories/channel/channel.v      | 14 +++++------
 theories/channel/proofmode.v    |  6 ++---
 theories/channel/proto.v        | 42 ++++++++++++++++-----------------
 theories/channel/proto_model.v  | 18 +++++++-------
 theories/examples/map_reduce.v  |  2 +-
 theories/logrel/contexts.v      | 10 ++++----
 theories/logrel/lib/list.v      |  2 +-
 theories/logrel/lib/mutex.v     |  4 ++--
 theories/logrel/model.v         |  6 ++---
 theories/logrel/session_types.v |  8 +++----
 theories/logrel/subtyping.v     |  6 ++---
 theories/logrel/term_types.v    | 20 ++++++++--------
 theories/utils/cofe_solver_2.v  |  2 +-
 theories/utils/contribution.v   |  4 ++--
 theories/utils/group.v          |  4 ++--
 15 files changed, 74 insertions(+), 74 deletions(-)

diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index 9e1380a..ee22902 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -71,18 +71,18 @@ Class chanG Σ := {
   chanG_protoG :> protoG Σ val;
 }.
 Definition chanΣ : gFunctors := #[ lockΣ; protoΣ val ].
-Instance subG_chanΣ {Σ} : subG chanΣ Σ → chanG Σ.
+Global Instance subG_chanΣ {Σ} : subG chanΣ Σ → chanG Σ.
 Proof. solve_inG. Qed.
 
 Record chan_name := ChanName {
   chan_lock_name : gname;
   chan_proto_name : proto_name;
 }.
-Instance chan_name_inhabited : Inhabited chan_name :=
+Global Instance chan_name_inhabited : Inhabited chan_name :=
   populate (ChanName inhabitant inhabitant).
-Instance chan_name_eq_dec : EqDecision chan_name.
+Global Instance chan_name_eq_dec : EqDecision chan_name.
 Proof. solve_decision. Qed.
-Instance chan_name_countable : Countable chan_name.
+Global Instance chan_name_countable : Countable chan_name.
 Proof.
  refine (inj_countable (λ '(ChanName γl γr), (γl,γr))
    (λ '(γl, γr), Some (ChanName γl γr)) _); by intros [].
@@ -106,11 +106,11 @@ Definition iProto_mapsto := iProto_mapsto_aux.(unseal).
 Definition iProto_mapsto_eq :
   @iProto_mapsto = @iProto_mapsto_def := iProto_mapsto_aux.(seal_eq).
 Arguments iProto_mapsto {_ _ _} _ _%proto.
-Instance: Params (@iProto_mapsto) 4 := {}.
+Global Instance: Params (@iProto_mapsto) 4 := {}.
 Notation "c ↣ p" := (iProto_mapsto c p)
   (at level 20, format "c  ↣  p").
 
-Instance iProto_mapsto_contractive `{!heapGS Σ, !chanG Σ} c :
+Global Instance iProto_mapsto_contractive `{!heapGS Σ, !chanG Σ} c :
   Contractive (iProto_mapsto c).
 Proof. rewrite iProto_mapsto_eq. solve_contractive. Qed.
 
@@ -119,7 +119,7 @@ Definition iProto_choice {Σ} (a : action) (P1 P2 : iProp Σ)
   (<a @ (b : bool)> MSG #b {{ if b then P1 else P2 }}; if b then p1 else p2)%proto.
 Typeclasses Opaque iProto_choice.
 Arguments iProto_choice {_} _ _%I _%I _%proto _%proto.
-Instance: Params (@iProto_choice) 2 := {}.
+Global Instance: Params (@iProto_choice) 2 := {}.
 Infix "<{ P1 }+{ P2 }>" := (iProto_choice Send P1 P2) (at level 85) : proto_scope.
 Infix "<{ P1 }&{ P2 }>" := (iProto_choice Recv P1 P2) (at level 85) : proto_scope.
 Infix "<+{ P2 }>" := (iProto_choice Send True P2) (at level 85) : proto_scope.
diff --git a/theories/channel/proofmode.v b/theories/channel/proofmode.v
index 8750ba4..ec00252 100644
--- a/theories/channel/proofmode.v
+++ b/theories/channel/proofmode.v
@@ -26,9 +26,9 @@ Class ActionDualIf (d : bool) (a1 a2 : action) :=
   dual_action_if : a2 = if d then action_dual a1 else a1.
 Global Hint Mode ActionDualIf ! ! - : typeclass_instances.
 
-Instance action_dual_if_false a : ActionDualIf false a a := eq_refl.
-Instance action_dual_if_true_send : ActionDualIf true Send Recv := eq_refl.
-Instance action_dual_if_true_recv : ActionDualIf true Recv Send := eq_refl.
+Global Instance action_dual_if_false a : ActionDualIf false a a := eq_refl.
+Global Instance action_dual_if_true_send : ActionDualIf true Send Recv := eq_refl.
+Global Instance action_dual_if_true_recv : ActionDualIf true Recv Send := eq_refl.
 
 Class ProtoNormalize {Σ} (d : bool) (p : iProto Σ)
     (pas : list (bool * iProto Σ)) (q : iProto Σ) :=
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index 111c9ee..b0b58bd 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -62,7 +62,7 @@ Class protoG Σ V :=
 Definition protoΣ V := #[
   GFunctor (authRF (optionURF (exclRF (laterOF (protoOF (leibnizO V) idOF idOF)))))
 ].
-Instance subG_chanΣ {Σ V} : subG (protoΣ V) Σ → protoG Σ V.
+Global Instance subG_chanΣ {Σ V} : subG (protoΣ V) Σ → protoG Σ V.
 Proof. solve_inG. Qed.
 
 (** * Types *)
@@ -83,7 +83,7 @@ Arguments iMsg_car {_ _} _.
 Declare Scope msg_scope.
 Delimit Scope msg_scope with msg.
 Bind Scope msg_scope with iMsg.
-Instance iMsg_inhabited {Σ V} : Inhabited (iMsg Σ V) := populate (IMsg inhabitant).
+Global Instance iMsg_inhabited {Σ V} : Inhabited (iMsg Σ V) := populate (IMsg inhabitant).
 
 Section imsg_ofe.
   Context {Σ : gFunctors} {V : Type}.
@@ -109,7 +109,7 @@ Definition iMsg_base_aux : seal (@iMsg_base_def). by eexists. Qed.
 Definition iMsg_base := iMsg_base_aux.(unseal).
 Definition iMsg_base_eq : @iMsg_base = @iMsg_base_def := iMsg_base_aux.(seal_eq).
 Arguments iMsg_base {_ _} _%V _%I _%proto.
-Instance: Params (@iMsg_base) 3 := {}.
+Global Instance: Params (@iMsg_base) 3 := {}.
 
 Program Definition iMsg_exist_def {Σ V A} (m : A → iMsg Σ V) : iMsg Σ V :=
   IMsg (λ v', λne p', ∃ x, iMsg_car (m x) v' p')%I.
@@ -118,7 +118,7 @@ Definition iMsg_exist_aux : seal (@iMsg_exist_def). by eexists. Qed.
 Definition iMsg_exist := iMsg_exist_aux.(unseal).
 Definition iMsg_exist_eq : @iMsg_exist = @iMsg_exist_def := iMsg_exist_aux.(seal_eq).
 Arguments iMsg_exist {_ _ _} _%msg.
-Instance: Params (@iMsg_exist) 3 := {}.
+Global Instance: Params (@iMsg_exist) 3 := {}.
 
 Definition iMsg_texist {Σ V} {TT : tele} (m : TT → iMsg Σ V) : iMsg Σ V :=
   tele_fold (@iMsg_exist Σ V) (λ x, x) (tele_bind m).
@@ -158,7 +158,7 @@ Definition iProto_message := iProto_message_aux.(unseal).
 Definition iProto_message_eq :
   @iProto_message = @iProto_message_def := iProto_message_aux.(seal_eq).
 Arguments iProto_message {_ _} _ _%msg.
-Instance: Params (@iProto_message) 3 := {}.
+Global Instance: Params (@iProto_message) 3 := {}.
 
 Notation "'END'" := iProto_end : proto_scope.
 
@@ -209,7 +209,7 @@ Next Obligation.
   apply proto_message_ne=> v p' /=. by repeat f_equiv.
 Qed.
 
-Instance iProto_map_app_aux_contractive {Σ V} f (p2 : iProto Σ V) :
+Global Instance iProto_map_app_aux_contractive {Σ V} f (p2 : iProto Σ V) :
   Contractive (iProto_map_app_aux f p2).
 Proof.
   intros n rec1 rec2 Hrec p1; simpl. apply proto_elim_ne=> // a m1 m2 Hm.
@@ -226,7 +226,7 @@ Definition iProto_app_aux : seal (@iProto_app_def). Proof. by eexists. Qed.
 Definition iProto_app := iProto_app_aux.(unseal).
 Definition iProto_app_eq : @iProto_app = @iProto_app_def := iProto_app_aux.(seal_eq).
 Arguments iProto_app {_ _} _%proto _%proto.
-Instance: Params (@iProto_app) 2 := {}.
+Global Instance: Params (@iProto_app) 2 := {}.
 Infix "<++>" := iProto_app (at level 60) : proto_scope.
 Notation "m <++> p" := (iMsg_map (flip iProto_app p) m) : msg_scope.
 
@@ -237,13 +237,13 @@ Definition iProto_dual := iProto_dual_aux.(unseal).
 Definition iProto_dual_eq :
   @iProto_dual = @iProto_dual_def := iProto_dual_aux.(seal_eq).
 Arguments iProto_dual {_ _} _%proto.
-Instance: Params (@iProto_dual) 2 := {}.
+Global Instance: Params (@iProto_dual) 2 := {}.
 Notation iMsg_dual := (iMsg_map iProto_dual).
 
 Definition iProto_dual_if {Σ V} (d : bool) (p : iProto Σ V) : iProto Σ V :=
   if d then iProto_dual p else p.
 Arguments iProto_dual_if {_ _} _ _%proto.
-Instance: Params (@iProto_dual_if) 3 := {}.
+Global Instance: Params (@iProto_dual_if) 3 := {}.
 
 (** * Protocol entailment *)
 Definition iProto_le_pre {Σ V}
@@ -261,7 +261,7 @@ Definition iProto_le_pre {Σ V}
          ▷ rec p1' (<!> MSG v2; pt) ∗ ▷ rec (<?> MSG v1; pt) p2'
     | Send, Recv => False
     end.
-Instance iProto_le_pre_ne {Σ V} (rec : iProto Σ V → iProto Σ V → iProp Σ) :
+Global Instance iProto_le_pre_ne {Σ V} (rec : iProto Σ V → iProto Σ V → iProp Σ) :
   NonExpansive2 (iProto_le_pre rec).
 Proof. solve_proper. Qed.
 
@@ -278,12 +278,12 @@ Qed.
 Definition iProto_le {Σ V} (p1 p2 : iProto Σ V) : iProp Σ :=
   fixpoint iProto_le_pre' p1 p2.
 Arguments iProto_le {_ _} _%proto _%proto.
-Instance: Params (@iProto_le) 2 := {}.
+Global Instance: Params (@iProto_le) 2 := {}.
 Notation "p ⊑ q" := (iProto_le p q) : bi_scope.
 
-Instance iProto_le_ne {Σ V} : NonExpansive2 (@iProto_le Σ V).
+Global Instance iProto_le_ne {Σ V} : NonExpansive2 (@iProto_le Σ V).
 Proof. solve_proper. Qed.
-Instance iProto_le_proper {Σ V} : Proper ((≡) ==> (≡) ==> (⊣⊢)) (@iProto_le Σ V).
+Global Instance iProto_le_proper {Σ V} : Proper ((≡) ==> (≡) ==> (⊣⊢)) (@iProto_le Σ V).
 Proof. solve_proper. Qed.
 
 Fixpoint iProto_app_recvs {Σ V} (vs : list V) (p : iProto Σ V) : iProto Σ V :=
@@ -295,21 +295,21 @@ Definition iProto_interp {Σ V} (vsl vsr : list V) (pl pr : iProto Σ V) : iProp
   ∃ p, iProto_app_recvs vsr p ⊑ pl ∗ iProto_app_recvs vsl (iProto_dual p) ⊑ pr.
 
 Record proto_name := ProtName { proto_l_name : gname; proto_r_name : gname }.
-Instance proto_name_inhabited : Inhabited proto_name :=
+Global Instance proto_name_inhabited : Inhabited proto_name :=
   populate (ProtName inhabitant inhabitant).
-Instance proto_name_eq_dec : EqDecision proto_name.
+Global Instance proto_name_eq_dec : EqDecision proto_name.
 Proof. solve_decision. Qed.
-Instance proto_name_countable : Countable proto_name.
+Global Instance proto_name_countable : Countable proto_name.
 Proof.
  refine (inj_countable (λ '(ProtName γl γr), (γl,γr))
    (λ '(γl, γr), Some (ProtName γl γr)) _); by intros [].
 Qed.
 
 Inductive side := Left | Right.
-Instance side_inhabited : Inhabited side := populate Left.
-Instance side_eq_dec : EqDecision side.
+Global Instance side_inhabited : Inhabited side := populate Left.
+Global Instance side_eq_dec : EqDecision side.
 Proof. solve_decision. Qed.
-Instance side_countable : Countable side.
+Global Instance side_countable : Countable side.
 Proof.
  refine (inj_countable (λ s, if s is Left then true else false)
    (λ b, Some (if b then Left else Right)) _); by intros [].
@@ -336,9 +336,9 @@ Definition iProto_own `{!protoG Σ V}
     (γ : proto_name) (s : side) (p : iProto Σ V) : iProp Σ :=
   ∃ p', ▷ (p' ⊑ p) ∗ iProto_own_frag γ s p'.
 Arguments iProto_own {_ _ _} _ _%proto.
-Instance: Params (@iProto_own) 3 := {}.
+Global Instance: Params (@iProto_own) 3 := {}.
 
-Instance iProto_own_contractive `{protoG Σ V} γ s :
+Global Instance iProto_own_contractive `{protoG Σ V} γ s :
   Contractive (iProto_own γ s).
 Proof. solve_contractive. Qed.
 
diff --git a/theories/channel/proto_model.v b/theories/channel/proto_model.v
index 5e600ef..37c8fd0 100644
--- a/theories/channel/proto_model.v
+++ b/theories/channel/proto_model.v
@@ -40,10 +40,10 @@ Set Default Proof Using "Type".
 
 Module Export action.
   Inductive action := Send | Recv.
-  Instance action_inhabited : Inhabited action := populate Send.
+  Global Instance action_inhabited : Inhabited action := populate Send.
   Definition action_dual (a : action) : action :=
     match a with Send => Recv | Recv => Send end.
-  Instance action_dual_involutive : Involutive (=) action_dual.
+  Global Instance action_dual_involutive : Involutive (=) action_dual.
   Proof. by intros []. Qed.
   Canonical Structure actionO := leibnizO action.
 End action.
@@ -56,7 +56,7 @@ Definition proto_auxOF (V : Type) (PROP : ofe) : oFunctor :=
 Definition proto_result (V : Type) := result_2 (proto_auxOF V).
 Definition proto (V : Type) (PROPn PROP : ofe) `{!Cofe PROPn, !Cofe PROP} : ofe :=
   solution_2_car (proto_result V) PROPn _ PROP _.
-Instance proto_cofe {V} `{!Cofe PROPn, !Cofe PROP} : Cofe (proto V PROPn PROP).
+Global Instance proto_cofe {V} `{!Cofe PROPn, !Cofe PROP} : Cofe (proto V PROPn PROP).
 Proof. apply _. Qed.
 Lemma proto_iso {V} `{!Cofe PROPn, !Cofe PROP} :
   ofe_iso (proto_auxO V PROP (proto V PROP PROPn)) (proto V PROPn PROP).
@@ -80,11 +80,11 @@ Definition proto_message {V} `{!Cofe PROPn, !Cofe PROP} (a : action)
     (m : V → laterO (proto V PROP PROPn) -n> PROP) : proto V PROPn PROP :=
   proto_fold (Some (a, m)).
 
-Instance proto_message_ne {V} `{!Cofe PROPn, !Cofe PROP} a n :
+Global Instance proto_message_ne {V} `{!Cofe PROPn, !Cofe PROP} a n :
   Proper (pointwise_relation V (dist n) ==> dist n)
          (proto_message (PROPn:=PROPn) (PROP:=PROP) a).
 Proof. intros c1 c2 Hc. rewrite /proto_message. f_equiv. by repeat constructor. Qed.
-Instance proto_message_proper {V} `{!Cofe PROPn, !Cofe PROP} a :
+Global Instance proto_message_proper {V} `{!Cofe PROPn, !Cofe PROP} a :
   Proper (pointwise_relation V (≡) ==> (≡))
          (proto_message (PROPn:=PROPn) (PROP:=PROP) a).
 Proof. intros c1 c2 Hc. rewrite /proto_message. f_equiv. by repeat constructor. Qed.
@@ -96,7 +96,7 @@ Proof.
   - left. by rewrite -(proto_fold_unfold p) E.
   - right. exists a, m. by rewrite /proto_message -E proto_fold_unfold.
 Qed.
-Instance proto_inhabited {V} `{!Cofe PROPn, !Cofe PROP} :
+Global Instance proto_inhabited {V} `{!Cofe PROPn, !Cofe PROP} :
   Inhabited (proto V PROPn PROP) := populate proto_end.
 
 Lemma proto_message_equivI `{!BiInternalEq SPROP} {V} `{!Cofe PROPn, !Cofe PROP} a1 a2 m1 m2 :
@@ -173,7 +173,7 @@ Next Obligation.
   apply proto_elim_ne=> // a m1 m2 Hm. by repeat f_equiv.
 Qed.
 
-Instance proto_map_aux_contractive {V}
+Global Instance proto_map_aux_contractive {V}
    `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'} (g : PROP -n> PROP') :
   Contractive (proto_map_aux (V:=V) (PROPn:=PROPn) (PROPn':=PROPn') g).
 Proof.
@@ -188,7 +188,7 @@ Definition proto_map_aux_2 {V}
     (rec : proto V PROPn PROP -n> proto V PROPn' PROP') :
     proto V PROPn PROP -n> proto V PROPn' PROP' :=
   proto_map_aux g (proto_map_aux gn rec).
-Instance proto_map_aux_2_contractive {V}
+Global Instance proto_map_aux_2_contractive {V}
    `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
     (gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
   Contractive (proto_map_aux_2 (V:=V) gn g).
@@ -294,7 +294,7 @@ Next Obligation.
   apply proto_map_ext=> //= y; by rewrite ofe.oFunctor_map_compose.
 Qed.
 
-Instance protoOF_contractive (V : Type) (Fn F : oFunctor)
+Global Instance protoOF_contractive (V : Type) (Fn F : oFunctor)
     `{!∀ A B `{!Cofe A, !Cofe B}, Cofe (oFunctor_car Fn A B)}
     `{!∀ A B `{!Cofe A, !Cofe B}, Cofe (oFunctor_car F A B)} :
   oFunctorContractive Fn → oFunctorContractive F → 
diff --git a/theories/examples/map_reduce.v b/theories/examples/map_reduce.v
index 9c3ae33..a06744b 100644
--- a/theories/examples/map_reduce.v
+++ b/theories/examples/map_reduce.v
@@ -9,7 +9,7 @@ From iris.algebra Require Import gmultiset.
 Definition map_reduce {A B C} `{EqDecision K}
     (map : A → list (K * B)) (red : K → list B → list C) : list A → list C :=
   mbind (curry red) ∘ group ∘ mbind map.
-Instance: Params (@map_reduce) 7 := {}.
+Global Instance: Params (@map_reduce) 7 := {}.
 
 (** * Distributed version (aka the implementation) *)
 Definition par_map_reduce_map : val :=
diff --git a/theories/logrel/contexts.v b/theories/logrel/contexts.v
index 805d299..fe0248a 100644
--- a/theories/logrel/contexts.v
+++ b/theories/logrel/contexts.v
@@ -24,8 +24,8 @@ Add Printing Constructor ctx_item.
 Arguments CtxItem {_} _ _.
 Arguments ctx_item_name {_} _.
 Arguments ctx_item_type {_} _.
-Instance: Params (@CtxItem) 2 := {}.
-Instance: Params (@ctx_item_type) 1 := {}.
+Global Instance: Params (@CtxItem) 2 := {}.
+Global Instance: Params (@ctx_item_type) 1 := {}.
 
 Section ctx_item_ofe.
   Context {Σ : gFunctors}.
@@ -58,7 +58,7 @@ Arguments ctx_filter_ne _ !_ !_ / : simpl nomatch.
 factored out. *)
 Arguments filter _ _ _ _ _ !_ / : simpl nomatch.
 
-Instance ctx_lookup {Σ} : Lookup string (ltty Σ) (ctx Σ) := λ x Γ,
+Global Instance ctx_lookup {Σ} : Lookup string (ltty Σ) (ctx Σ) := λ x Γ,
   match ctx_filter_eq x Γ with
   | [CtxItem _ A] => Some A
   | _ => None
@@ -70,11 +70,11 @@ Definition ctx_cons {Σ} (b : binder) (A : ltty Σ) (Γ : ctx Σ) : ctx Σ :=
 Definition ctx_ltyped {Σ} (vs : gmap string val) (Γ : ctx Σ) : iProp Σ :=
   ([∗ list] iA ∈ Γ, ∃ v,
     ⌜vs !! ctx_item_name iA = Some v⌝ ∗ ltty_car (ctx_item_type iA) v)%I.
-Instance: Params (@ctx_ltyped) 2 := {}.
+Global Instance: Params (@ctx_ltyped) 2 := {}.
 
 Definition ctx_le {Σ} (Γ1 Γ2 : ctx Σ) : iProp Σ :=
   tc_opaque (■ ∀ vs, ctx_ltyped vs Γ1 -∗ ctx_ltyped vs Γ2)%I.
-Instance: Params (@ctx_le) 1 := {}.
+Global Instance: Params (@ctx_le) 1 := {}.
 Infix "<ctx:" := ctx_le (at level 70) : bi_scope.
 Notation "Γ1 <ctx: Γ2" := (⊢ Γ1 <ctx: Γ2) (at level 70) : type_scope.
 
diff --git a/theories/logrel/lib/list.v b/theories/logrel/lib/list.v
index 3f5e646..870e4fd 100644
--- a/theories/logrel/lib/list.v
+++ b/theories/logrel/lib/list.v
@@ -4,7 +4,7 @@ From actris.logrel Require Import term_types.
 
 Definition lty_list_aux `{!heapGS Σ} (A : ltty Σ) (X : ltty Σ) : ltty Σ :=
   ref_uniq (() + (A * X)).
-Instance lty_list_aux_contractive `{!heapGS Σ} A :
+Global Instance lty_list_aux_contractive `{!heapGS Σ} A :
   Contractive (@lty_list_aux Σ _ A).
 Proof. solve_proto_contractive. Qed.
 Definition lty_list `{!heapGS Σ} (A : ltty Σ) : ltty Σ := lty_rec (lty_list_aux A).
diff --git a/theories/logrel/lib/mutex.v b/theories/logrel/lib/mutex.v
index 9e2d515..eb5ca71 100644
--- a/theories/logrel/lib/mutex.v
+++ b/theories/logrel/lib/mutex.v
@@ -47,8 +47,8 @@ Definition lty_mutex_guard `{heapGS Σ, lockG Σ} (A : ltty Σ) : ltty Σ := Ltt
     is_lock γ lk (∃ v_inner, l ↦ v_inner ∗ ltty_car A v_inner) ∗
     spin_lock.locked γ ∗ l ↦ v)%I.
 
-Instance: Params (@lty_mutex) 3 := {}.
-Instance: Params (@lty_mutex_guard) 3 := {}.
+Global Instance: Params (@lty_mutex) 3 := {}.
+Global Instance: Params (@lty_mutex_guard) 3 := {}.
 
 Notation "'mutex' A" := (lty_mutex A) (at level 10) : lty_scope.
 Notation "'mutex_guard' A" := (lty_mutex_guard A) (at level 10) : lty_scope.
diff --git a/theories/logrel/model.v b/theories/logrel/model.v
index 78465e9..25adfad 100644
--- a/theories/logrel/model.v
+++ b/theories/logrel/model.v
@@ -16,9 +16,9 @@ From iris.algebra Require Export ofe.
 From actris.channel Require Export channel.
 
 Inductive kind := tty_kind | sty_kind.
-Instance kind_eq_dec : EqDecision kind.
+Global Instance kind_eq_dec : EqDecision kind.
 Proof. solve_decision. Defined.
-Instance kind_inhabited : Inhabited kind := populate tty_kind.
+Global Instance kind_inhabited : Inhabited kind := populate tty_kind.
 
 (** Use [Variant] to suppress generation of induction schemes *)
 Variant lty Σ : kind → Type :=
@@ -41,7 +41,7 @@ Definition lsty_car {Σ} (p : lsty Σ) : iProto Σ :=
 Arguments ltty_car {_} _ _ : simpl never.
 Arguments lsty_car {_} _ : simpl never.
 
-Instance lty_inhabited Σ k : Inhabited (lty Σ k) := populate $
+Global Instance lty_inhabited Σ k : Inhabited (lty Σ k) := populate $
   match k with
   | tty_kind => Ltty inhabitant
   | lty_kind => Lsty inhabitant
diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index d04230c..23b5054 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -34,10 +34,10 @@ Definition lty_dual {Σ} (S : lsty Σ) : lsty Σ :=
 Definition lty_app {Σ} (S1 S2 : lsty Σ) : lsty Σ :=
   Lsty (lsty_car S1 <++> lsty_car S2).
 
-Instance: Params (@lty_message) 2 := {}.
-Instance: Params (@lty_choice) 2 := {}.
-Instance: Params (@lty_dual) 1 := {}.
-Instance: Params (@lty_app) 1 := {}.
+Global Instance: Params (@lty_message) 2 := {}.
+Global Instance: Params (@lty_choice) 2 := {}.
+Global Instance: Params (@lty_dual) 1 := {}.
+Global Instance: Params (@lty_app) 1 := {}.
 
 Notation "'TY' A ; S" := (lty_msg_base A S)
   (at level 200, right associativity,
diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index 69acaac..178951b 100644
--- a/theories/logrel/subtyping.v
+++ b/theories/logrel/subtyping.v
@@ -13,18 +13,18 @@ Definition lty_le {Σ k} : lty Σ k → lty Σ k → iProp Σ :=
 Arguments lty_le : simpl never.
 Infix "<:" := lty_le (at level 70) : bi_scope.
 Notation "K1 <: K2" := (⊢ K1 <: K2) (at level 70) : type_scope.
-Instance: Params (@lty_le) 2 := {}.
+Global Instance: Params (@lty_le) 2 := {}.
 
 Definition lty_bi_le {Σ k} (M1 M2 : lty Σ k) : iProp Σ :=
   tc_opaque (M1 <: M2 ∧ M2 <: M1)%I.
 Arguments lty_bi_le : simpl never.
 Infix "<:>" := lty_bi_le (at level 70) : bi_scope.
 Notation "K1 <:> K2" := (⊢ K1 <:> K2) (at level 70) : type_scope.
-Instance: Params (@lty_bi_le) 2 := {}.
+Global Instance: Params (@lty_bi_le) 2 := {}.
 
 Definition lty_copyable {Σ} (A : ltty Σ) : iProp Σ :=
   tc_opaque (A <: lty_copy A)%I.
-Instance: Params (@lty_copyable) 1 := {}.
+Global Instance: Params (@lty_copyable) 1 := {}.
 
 Section subtyping.
   Context {Σ : gFunctors}.
diff --git a/theories/logrel/term_types.v b/theories/logrel/term_types.v
index 615562c..1b6a178 100644
--- a/theories/logrel/term_types.v
+++ b/theories/logrel/term_types.v
@@ -69,16 +69,16 @@ Definition lty_ref_shr `{heapGS Σ} (A : ltty Σ) : ltty Σ := Ltty (λ w,
 Definition lty_chan `{heapGS Σ, chanG Σ} (P : lsty Σ) : ltty Σ :=
   Ltty (λ w, w ↣ lsty_car P)%I.
 
-Instance: Params (@lty_copy) 1 := {}.
-Instance: Params (@lty_copy_minus) 1 := {}.
-Instance: Params (@lty_arr) 2 := {}.
-Instance: Params (@lty_prod) 1 := {}.
-Instance: Params (@lty_sum) 1 := {}.
-Instance: Params (@lty_forall) 2 := {}.
-Instance: Params (@lty_sum) 1 := {}.
-Instance: Params (@lty_ref_uniq) 2 := {}.
-Instance: Params (@lty_ref_shr) 2 := {}.
-Instance: Params (@lty_chan) 3 := {}.
+Global Instance: Params (@lty_copy) 1 := {}.
+Global Instance: Params (@lty_copy_minus) 1 := {}.
+Global Instance: Params (@lty_arr) 2 := {}.
+Global Instance: Params (@lty_prod) 1 := {}.
+Global Instance: Params (@lty_sum) 1 := {}.
+Global Instance: Params (@lty_forall) 2 := {}.
+Global Instance: Params (@lty_sum) 1 := {}.
+Global Instance: Params (@lty_ref_uniq) 2 := {}.
+Global Instance: Params (@lty_ref_shr) 2 := {}.
+Global Instance: Params (@lty_chan) 3 := {}.
 
 Notation any := lty_any.
 Notation "()" := lty_unit : lty_scope.
diff --git a/theories/utils/cofe_solver_2.v b/theories/utils/cofe_solver_2.v
index 6e05519..91b37df 100644
--- a/theories/utils/cofe_solver_2.v
+++ b/theories/utils/cofe_solver_2.v
@@ -9,7 +9,7 @@ Record solution_2 (F : ofe → oFunctor) := Solution2 {
     ofe_iso (oFunctor_apply (F A) (solution_2_car A An)) (solution_2_car An A);
 }.
 Arguments solution_2_car {F}.
-Existing Instance solution_2_cofe.
+Global Existing Instance solution_2_cofe.
 
 Section cofe_solver_2.
   Context (F : ofe → oFunctor).
diff --git a/theories/utils/contribution.v b/theories/utils/contribution.v
index 2676fdb..1a7d3af 100644
--- a/theories/utils/contribution.v
+++ b/theories/utils/contribution.v
@@ -30,12 +30,12 @@ Definition server `{contributionG Σ A} (γ : gname) (n : nat) (x : A) : iProp 
    then x ≡ ε ∗ own γ (● (Some (Cinr (Excl ())))) ∗ own γ (◯ (Some (Cinr (Excl ()))))
    else own γ (● (Some (Cinl (Pos.of_nat n, x)))))%I.
 Typeclasses Opaque server.
-Instance: Params (@server) 6 := {}.
+Global Instance: Params (@server) 6 := {}.
 
 Definition client `{contributionG Σ A} (γ : gname) (x : A) : iProp Σ :=
   own γ (◯ (Some (Cinl (1%positive, x)))).
 Typeclasses Opaque client.
-Instance: Params (@client) 5 := {}.
+Global Instance: Params (@client) 5 := {}.
 
 Section contribution.
   Context `{contributionG Σ A}.
diff --git a/theories/utils/group.v b/theories/utils/group.v
index 92791a5..4397bd1 100644
--- a/theories/utils/group.v
+++ b/theories/utils/group.v
@@ -17,8 +17,8 @@ Fixpoint group {A} `{EqDecision K} (ixs : list (K * A)) : list (K * list A) :=
   | (i,x) :: ixs => group_insert i x (group ixs)
   end.
 
-Instance: Params (@group_insert) 5 := {}.
-Instance: Params (@group) 3 := {}.
+Global Instance: Params (@group_insert) 5 := {}.
+Global Instance: Params (@group) 3 := {}.
 
 Local Infix "≡ₚₚ" :=
   (PermutationA (prod_relation (=) (≡ₚ))) (at level 70, no associativity) : stdpp_scope.
-- 
GitLab