From 9e137e44215b2601c2cdf5433a8aa4646b11a0ce Mon Sep 17 00:00:00 2001
From: Yusuke Matsushita <y.skm24t@gmail.com>
Date: Thu, 21 Apr 2022 02:25:53 +0900
Subject: [PATCH] Add more Global markers

---
 theories/lang/adequacy.v              |  2 +-
 theories/lang/heap.v                  |  2 +-
 theories/lang/lang.v                  | 24 ++++++------
 theories/lang/lib/arc.v               |  2 +-
 theories/lang/lib/lock.v              |  2 +-
 theories/lang/lib/spawn.v             |  4 +-
 theories/lang/lifting.v               | 12 +++---
 theories/lang/time.v                  |  2 +-
 theories/lifetime/at_borrow.v         |  2 +-
 theories/lifetime/frac_borrow.v       |  2 +-
 theories/lifetime/lifetime.v          |  2 +-
 theories/lifetime/lifetime_sig.v      |  2 +-
 theories/lifetime/model/definitions.v | 18 ++++-----
 theories/lifetime/model/primitive.v   | 16 ++++----
 theories/lifetime/na_borrow.v         |  2 +-
 theories/typing/function.v            |  4 +-
 theories/typing/lib/arc.v             |  2 +-
 theories/typing/lib/rc/rc.v           |  2 +-
 theories/typing/lib/refcell/refcell.v |  2 +-
 theories/typing/lib/rwlock/rwlock.v   |  2 +-
 theories/typing/soundness.v           |  2 +-
 theories/typing/type.v                | 56 +++++++++++++--------------
 theories/typing/type_context.v        |  8 ++--
 theories/util/basic.v                 |  2 +-
 theories/util/fancy_lists.v           | 10 ++---
 25 files changed, 92 insertions(+), 92 deletions(-)

diff --git a/theories/lang/adequacy.v b/theories/lang/adequacy.v
index 152c5a6a..cc7600f2 100644
--- a/theories/lang/adequacy.v
+++ b/theories/lang/adequacy.v
@@ -16,7 +16,7 @@ Definition lrustΣ : gFunctors :=
   #[invΣ; timeΣ;
     GFunctor (constRF (authR heapUR));
     GFunctor (constRF (authR heap_freeableUR))].
-Instance subG_heapPreG {Σ} : subG lrustΣ Σ → lrustGpreS Σ.
+Global Instance subG_heapPreG {Σ} : subG lrustΣ Σ → lrustGpreS Σ.
 Proof. solve_inG. Qed.
 
 Definition lrust_adequacy Σ `{!lrustGpreS Σ} e σ φ :
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 5fe4d602..80758c14 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -66,7 +66,7 @@ Section definitions.
          ∗ ⌜heap_freeable_rel σ hF⌝)%I.
 End definitions.
 
-Typeclasses Opaque heap_mapsto heap_freeable heap_mapsto_vec.
+Global Typeclasses Opaque heap_mapsto heap_freeable heap_mapsto_vec.
 Global Instance: Params (@heap_mapsto) 4 := {}.
 Global Instance: Params (@heap_freeable) 5 := {}.
 
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index c0cbcef9..d2b59983 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -60,9 +60,9 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
   end.
 
 Class Closed (X : list string) (e : expr) := closed : is_closed X e.
-Instance closed_proof_irrel env e : ProofIrrel (Closed env e).
+Global Instance closed_proof_irrel env e : ProofIrrel (Closed env e).
 Proof. rewrite /Closed. apply _. Qed.
-Instance closed_decision env e : Decision (Closed env e).
+Global Instance closed_decision env e : Decision (Closed env e).
 Proof. rewrite /Closed. apply _. Qed.
 
 Inductive val :=
@@ -352,10 +352,10 @@ Proof.
   revert v; induction e; intros v ?; simplify_option_eq; auto with f_equal.
 Qed.
 
-Instance of_val_inj : Inj (=) (=) of_val.
+Global Instance of_val_inj : Inj (=) (=) of_val.
 Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
 
-Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
+Global Instance fill_item_inj Ki : Inj (=) (=) (fill_item Ki).
 Proof. destruct Ki; intros ???; simplify_eq/=; auto with f_equal. Qed.
 
 Lemma fill_item_val Ki e :
@@ -408,7 +408,7 @@ Proof. rewrite /shift_loc /=. f_equal. lia. Qed.
 Lemma shift_loc_0_nat l : l +ₗ 0%nat = l.
 Proof. destruct l as [b o]. rewrite /shift_loc /=. f_equal. lia. Qed.
 
-Instance shift_loc_inj l : Inj (=) (=) (shift_loc l).
+Global Instance shift_loc_inj l : Inj (=) (=) (shift_loc l).
 Proof. destruct l as [b o]; intros n n' [=?]; lia. Qed.
 
 Lemma shift_loc_block l n : (l +ₗ n).1 = l.1.
@@ -542,11 +542,11 @@ Lemma stuck_not_head_step σ e' κ σ' ef :
 Proof. inversion 1. Qed.
 
 (** Equality and other typeclass stuff *)
-Instance base_lit_dec_eq : EqDecision base_lit.
+Global Instance base_lit_dec_eq : EqDecision base_lit.
 Proof. solve_decision. Defined.
-Instance bin_op_dec_eq : EqDecision bin_op.
+Global Instance bin_op_dec_eq : EqDecision bin_op.
 Proof. solve_decision. Defined.
-Instance un_op_dec_eq : EqDecision order.
+Global Instance un_op_dec_eq : EqDecision order.
 Proof. solve_decision. Defined.
 
 Fixpoint expr_beq (e : expr) (e' : expr) : bool :=
@@ -592,17 +592,17 @@ Proof.
       specialize (FIX el1h). naive_solver. }
     clear FIX. naive_solver.
 Qed.
-Instance expr_dec_eq : EqDecision expr.
+Global Instance expr_dec_eq : EqDecision expr.
 Proof.
  refine (λ e1 e2, cast_if (decide (expr_beq e1 e2))); by rewrite -expr_beq_correct.
 Defined.
-Instance val_dec_eq : EqDecision val.
+Global Instance val_dec_eq : EqDecision val.
 Proof.
  refine (λ v1 v2, cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver.
 Defined.
 
-Instance expr_inhabited : Inhabited expr := populate (Lit LitPoison).
-Instance val_inhabited : Inhabited val := populate (LitV LitPoison).
+Global Instance expr_inhabited : Inhabited expr := populate (Lit LitPoison).
+Global Instance val_inhabited : Inhabited val := populate (LitV LitPoison).
 
 Canonical Structure stateO := leibnizO state.
 Canonical Structure valO := leibnizO val.
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index 8c897d67..63d8295c 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -669,4 +669,4 @@ Section arc.
   Qed.
 End arc.
 
-Typeclasses Opaque is_arc arc_tok weak_tok.
+Global Typeclasses Opaque is_arc arc_tok weak_tok.
diff --git a/theories/lang/lib/lock.v b/theories/lang/lib/lock.v
index 2ab7a9f3..e62a6e5f 100644
--- a/theories/lang/lib/lock.v
+++ b/theories/lang/lib/lock.v
@@ -109,4 +109,4 @@ Section proof.
   Qed.
 End proof.
 
-Typeclasses Opaque lock_proto.
+Global Typeclasses Opaque lock_proto.
diff --git a/theories/lang/lib/spawn.v b/theories/lang/lib/spawn.v
index 66ad5d22..3b21e980 100644
--- a/theories/lang/lib/spawn.v
+++ b/theories/lang/lib/spawn.v
@@ -31,7 +31,7 @@ Definition join : val :=
 Class spawnG Σ := SpawnG { spawn_tokG :> inG Σ (exclR unitO) }.
 Definition spawnΣ : gFunctors := #[GFunctor (exclR unitO)].
 
-Instance subG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ.
+Global Instance subG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ.
 Proof. solve_inG. Qed.
 
 (** Now we come to the Iris part of the proof. *)
@@ -125,4 +125,4 @@ Qed.
 
 End proof.
 
-Typeclasses Opaque finish_handle join_handle.
+Global Typeclasses Opaque finish_handle join_handle.
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index 844d971d..4c263e3d 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -12,7 +12,7 @@ Class lrustGS Σ := LRustGS {
   lrustGS_gen_timeGS :> timeGS Σ
 }.
 
-Program Instance lrustGS_irisGS `{!lrustGS Σ} : irisGS lrust_lang Σ := {
+Global Program Instance lrustGS_irisGS `{!lrustGS Σ} : irisGS lrust_lang Σ := {
   iris_invGS := lrustGS_invGS;
   state_interp σ stepcnt κs _ := (heap_ctx σ ∗ time_interp stepcnt)%I;
   fork_post _ := True%I;
@@ -44,8 +44,8 @@ Local Hint Resolve to_of_val : core.
 
 Class AsRec (e : expr) (f : binder) (xl : list binder) (erec : expr) :=
   as_rec : e = Rec f xl erec.
-Instance AsRec_rec f xl e : AsRec (Rec f xl e) f xl e := eq_refl.
-Instance AsRec_rec_locked_val v f xl e :
+Global Instance AsRec_rec f xl e : AsRec (Rec f xl e) f xl e := eq_refl.
+Global Instance AsRec_rec_locked_val v f xl e :
   AsRec (of_val v) f xl e → AsRec (of_val (locked v)) f xl e.
 Proof. by unlock. Qed.
 
@@ -56,13 +56,13 @@ Global Hint Extern 0 (DoSubst _ _ _ _) =>
 
 Class DoSubstL (xl : list binder) (esl : list expr) (e er : expr) :=
   do_subst_l : subst_l xl esl e = Some er.
-Instance do_subst_l_nil e : DoSubstL [] [] e e.
+Global Instance do_subst_l_nil e : DoSubstL [] [] e e.
 Proof. done. Qed.
-Instance do_subst_l_cons x xl es esl e er er' :
+Global Instance do_subst_l_cons x xl es esl e er er' :
   DoSubstL xl esl e er' → DoSubst x es er' er →
   DoSubstL (x :: xl) (es :: esl) e er.
 Proof. rewrite /DoSubstL /DoSubst /= => -> <- //. Qed.
-Instance do_subst_vec xl (vsl : vec val (length xl)) e :
+Global Instance do_subst_vec xl (vsl : vec val (length xl)) e :
   DoSubstL xl (of_val <$> vec_to_list vsl) e (subst_v xl vsl e).
 Proof. by rewrite /DoSubstL subst_v_eq. Qed.
 
diff --git a/theories/lang/time.v b/theories/lang/time.v
index 3e26718a..c40fd603 100644
--- a/theories/lang/time.v
+++ b/theories/lang/time.v
@@ -21,7 +21,7 @@ Class timePreG Σ := TimePreG {
 
 Definition timeΣ : gFunctors :=
   #[GFunctor (constRF mono_natR); GFunctor (constRF (authR natUR))].
-Instance subG_timePreG Σ : subG timeΣ Σ → timePreG Σ.
+Global Instance subG_timePreG Σ : subG timeΣ Σ → timePreG Σ.
 Proof. solve_inG. Qed.
 
 Definition timeN : namespace := nroot .@ "lft_usr" .@ "time".
diff --git a/theories/lifetime/at_borrow.v b/theories/lifetime/at_borrow.v
index 091ab883..a0c5e574 100644
--- a/theories/lifetime/at_borrow.v
+++ b/theories/lifetime/at_borrow.v
@@ -103,4 +103,4 @@ Lemma at_bor_acc_lftN `{!invGS Σ, !lftGS Σ} (P : iProp Σ) E κ :
              [†κ] ∗ |={E∖↑lftN,E}=> True.
 Proof. intros. by rewrite (at_bor_acc _ lftN) // difference_twice_L. Qed.
 
-Typeclasses Opaque at_bor.
+Global Typeclasses Opaque at_bor.
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index d0475952..2d377558 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -168,4 +168,4 @@ Proof.
     iDestruct (lft_tok_dead with "Hκ' H†'") as "[]".
 Qed.
 
-Typeclasses Opaque frac_bor.
+Global Typeclasses Opaque frac_bor.
diff --git a/theories/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index a184733f..b4fd5655 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -26,7 +26,7 @@ Proof.
   - by rewrite /= IH assoc.
 Qed.
 
-Instance lft_inhabited : Inhabited lft := populate static.
+Global Instance lft_inhabited : Inhabited lft := populate static.
 
 Canonical lftO := leibnizO lft.
 
diff --git a/theories/lifetime/lifetime_sig.v b/theories/lifetime/lifetime_sig.v
index 5f94a63c..5feadc30 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -25,7 +25,7 @@ Module Type lifetime_sig.
   (** Definitions *)
   Parameter lft : Type.
   Parameter static : lft.
-  Declare Instance lft_intersect : Meet lft.
+  Global Declare Instance lft_intersect : Meet lft.
 
   Parameter lft_ctx : ∀ `{!invGS Σ, !lftGS Σ}, iProp Σ.
 
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index fcb5f0fc..63070fd0 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -17,7 +17,7 @@ Module Export lft_notation.
 End lft_notation.
 
 Definition static : lft := (∅ : gmultiset _).
-Instance lft_intersect : Meet lft := λ κ κ', κ ⊎ κ'.
+Global Instance lft_intersect : Meet lft := λ κ κ', κ ⊎ κ'.
 
 Inductive bor_state :=
   | Bor_in
@@ -63,7 +63,7 @@ Definition lftGpreS' := lftGpreS.
 Definition lftΣ : gFunctors :=
   #[ boxΣ; GFunctor (authR alftUR); GFunctor (authR ilftUR);
      GFunctor (authR borUR); GFunctor (authR natUR); GFunctor (authR inhUR) ].
-Instance subG_lftGpreS Σ :
+Global Instance subG_lftGpreS Σ :
   subG lftΣ Σ → lftGpreS Σ.
 Proof. solve_inG. Qed.
 
@@ -197,12 +197,12 @@ Section defs.
     (∃ κ', lft_incl κ κ' ∗ raw_bor κ' P)%I.
 End defs.
 
-Instance: Params (@lft_bor_alive) 4 := {}.
-Instance: Params (@lft_inh) 5 := {}.
-Instance: Params (@lft_vs) 4 := {}.
-Instance idx_bor_params : Params (@idx_bor) 5 := {}.
-Instance raw_bor_params : Params (@raw_bor) 4 := {}.
-Instance bor_params : Params (@bor) 4 := {}.
+Global Instance: Params (@lft_bor_alive) 4 := {}.
+Global Instance: Params (@lft_inh) 5 := {}.
+Global Instance: Params (@lft_vs) 4 := {}.
+Global Instance idx_bor_params : Params (@idx_bor) 5 := {}.
+Global Instance raw_bor_params : Params (@raw_bor) 4 := {}.
+Global Instance bor_params : Params (@bor) 4 := {}.
 
 Notation "q .[ κ ]" := (lft_tok q κ)
     (format "q .[ κ ]", at level 2, left associativity) : bi_scope.
@@ -216,7 +216,7 @@ Infix "⊑" := lft_incl (at level 70) : bi_scope.
 (* TODO: Making all these things opaque is rather annoying, we should
    find a way to avoid it, or *at least*, to avoid having to manually unfold
    this because iDestruct et al don't look through these names any more. *)
-Typeclasses Opaque lft_tok lft_dead bor_cnt lft_bor_alive lft_bor_dead
+Global Typeclasses Opaque lft_tok lft_dead bor_cnt lft_bor_alive lft_bor_dead
   lft_inh lft_inv_alive lft_vs_inv lft_vs lft_inv_dead lft_inv lft_incl
   idx_bor_own idx_bor raw_bor bor.
 
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 547d293a..9909792b 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -254,14 +254,14 @@ Proof.
 Qed.
 
 (** Basic rules about lifetimes  *)
-Instance lft_inhabited : Inhabited lft := _.
-Instance bor_idx_inhabited : Inhabited bor_idx := _.
-Instance lft_intersect_comm : Comm (A:=lft) eq (⊓) := _.
-Instance lft_intersect_assoc : Assoc (A:=lft) eq (⊓) := _.
-Instance lft_intersect_inj_1 κ : Inj eq eq (κ ⊓.) := _.
-Instance lft_intersect_inj_2 κ : Inj eq eq (.⊓ κ) := _.
-Instance lft_intersect_left_id : LeftId eq static (⊓) := _.
-Instance lft_intersect_right_id : RightId eq static (⊓) := _.
+Global Instance lft_inhabited : Inhabited lft := _.
+Global Instance bor_idx_inhabited : Inhabited bor_idx := _.
+Global Instance lft_intersect_comm : Comm (A:=lft) eq (⊓) := _.
+Global Instance lft_intersect_assoc : Assoc (A:=lft) eq (⊓) := _.
+Global Instance lft_intersect_inj_1 κ : Inj eq eq (κ ⊓.) := _.
+Global Instance lft_intersect_inj_2 κ : Inj eq eq (.⊓ κ) := _.
+Global Instance lft_intersect_left_id : LeftId eq static (⊓) := _.
+Global Instance lft_intersect_right_id : RightId eq static (⊓) := _.
 
 Lemma lft_tok_sep q κ1 κ2 : q.[κ1] ∗ q.[κ2] ⊣⊢ q.[κ1 ⊓ κ2].
 Proof. by rewrite /lft_tok -big_sepMS_disj_union. Qed.
diff --git a/theories/lifetime/na_borrow.v b/theories/lifetime/na_borrow.v
index f9b5932e..2b629348 100644
--- a/theories/lifetime/na_borrow.v
+++ b/theories/lifetime/na_borrow.v
@@ -63,4 +63,4 @@ Section na_bor.
   Qed.
 End na_bor.
 
-Typeclasses Opaque na_bor.
+Global Typeclasses Opaque na_bor.
diff --git a/theories/typing/function.v b/theories/typing/function.v
index cbabd1f0..85fdee56 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -11,7 +11,7 @@ Fixpoint subst_plv {𝔄l} (bl: plistc binder 𝔄l) (vl: plistc val 𝔄l) (e:
   | _::_, b -:: bl', v -:: vl' => subst' b v (subst_plv bl' vl' e)
   end.
 
-Instance do_subst_plv {𝔄l} (bl vl: plistc _ 𝔄l) e :
+Global Instance do_subst_plv {𝔄l} (bl vl: plistc _ 𝔄l) e :
   DoSubstL bl (map of_val vl) e (subst_plv bl vl e).
 Proof.
   rewrite /DoSubstL. induction 𝔄l, bl, vl; [done|]=>/=. by rewrite IH𝔄l.
@@ -94,7 +94,7 @@ End fn.
 
 Arguments fn_params {_ _} _ _.
 
-Instance elctx_empty : Empty (lft → elctx) := λ _, [].
+Global Instance elctx_empty : Empty (lft → elctx) := λ _, [].
 
 Notation "fn< p > ( E ; ity , .. , ity' ) → oty" :=
   (fn (λ p, FP E%EL (ity%T +:: .. (+[ity'%T]) ..) oty%T))
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index b6c1510d..0d0bfc40 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -17,7 +17,7 @@ Section arc.
 
   (* Preliminary definitions. *)
   Let P1 ν q := (q.[ν])%I.
-  Instance P1_fractional ν : Fractional (P1 ν).
+  Global Instance P1_fractional ν : Fractional (P1 ν).
   Proof. unfold P1. apply _. Qed.
   Let P2 l n := († l…(2 + n) ∗ (l +ₗ 2) ↦∗: λ vl, ⌜length vl = n⌝)%I.
   Definition arc_persist tid ν (γ : gname) (l : loc) (ty : type) : iProp Σ :=
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 989138bd..15b85b12 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -11,7 +11,7 @@ Definition rc_stR :=
 Class rcG Σ :=
   RcG :> inG Σ (authR rc_stR).
 Definition rcΣ : gFunctors := #[GFunctor (authR rc_stR)].
-Instance subG_rcΣ {Σ} : subG rcΣ Σ → rcG Σ.
+Global Instance subG_rcΣ {Σ} : subG rcΣ Σ → rcG Σ.
 Proof. solve_inG. Qed.
 
 Definition rc_tok q : authR rc_stR :=
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index 5573e83f..8af8e2c4 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -13,7 +13,7 @@ Definition refcell_stR :=
 Class refcellG Σ :=
   RefCellG :> inG Σ (authR refcell_stR).
 Definition refcellΣ : gFunctors := #[GFunctor (authR refcell_stR)].
-Instance subG_refcellΣ {Σ} : subG refcellΣ Σ → refcellG Σ.
+Global Instance subG_refcellΣ {Σ} : subG refcellΣ Σ → refcellG Σ.
 Proof. solve_inG. Qed.
 
 Definition refcell_st := option ((lft * Datatypes.bool) * frac * positive).
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index 736d26ed..1b48d479 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -10,7 +10,7 @@ Definition rwlock_stR :=
 Class rwlockG Σ :=
   RwLockG :> inG Σ (authR rwlock_stR).
 Definition rwlockΣ : gFunctors := #[GFunctor (authR rwlock_stR)].
-Instance subG_rwlockΣ {Σ} : subG rwlockΣ Σ → rwlockG Σ.
+Global Instance subG_rwlockΣ {Σ} : subG rwlockΣ Σ → rwlockG Σ.
 Proof. solve_inG. Qed.
 
 Definition Z_of_rwlock_st (st : rwlock_stR) : Z :=
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index c86c4f30..fa15c7fa 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -18,7 +18,7 @@ Class typePreG Σ := PreTypeG {
 Definition typeΣ : gFunctors :=
   #[lrustΣ; lftΣ; na_invΣ;
     GFunctor (constRF fracR); uniqΣ; prophΣ].
-Instance subG_typePreG {Σ} : subG typeΣ Σ → typePreG Σ.
+Global Instance subG_typePreG {Σ} : subG typeΣ Σ → typePreG Σ.
 Proof. solve_inG. Qed.
 
 Section type_soundness.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 401d5979..47be8272 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -67,12 +67,12 @@ Record type `{!typeG Σ} 𝔄 := {
     ={E}▷=∗ |={E}▷=>^d |={E}=> ∃ξl q', ⌜vπ ./ ξl⌝ ∗
       q':+[ξl] ∗ (q':+[ξl] ={E}=∗ q.[κ']);
 }.
-Existing Instance ty_shr_persistent.
-Instance: Params (@ty_size) 3 := {}.
-Instance: Params (@ty_lfts) 3 := {}.
-Instance: Params (@ty_E) 3 := {}.
-Instance: Params (@ty_own) 3 := {}.
-Instance: Params (@ty_shr) 3 := {}.
+Global Existing Instance ty_shr_persistent.
+Global Instance: Params (@ty_size) 3 := {}.
+Global Instance: Params (@ty_lfts) 3 := {}.
+Global Instance: Params (@ty_E) 3 := {}.
+Global Instance: Params (@ty_own) 3 := {}.
+Global Instance: Params (@ty_shr) 3 := {}.
 Arguments ty_size {_ _ _} _ / : simpl nomatch.
 Arguments ty_lfts {_ _ _} _ / : simpl nomatch.
 Arguments ty_E {_ _ _} _ / : simpl nomatch.
@@ -175,11 +175,11 @@ Record simple_type `{!typeG Σ} 𝔄 := {
     ={E}=∗ |={E}▷=>^d |={E}=> ∃ξl q', ⌜vπ ./ ξl⌝ ∗
       q':+[ξl] ∗ (q':+[ξl] ={E}=∗ st_own vπ d tid vl ∗ q.[κ]);
 }.
-Existing Instance st_own_persistent.
-Instance: Params (@st_size) 3 := {}.
-Instance: Params (@st_lfts) 3 := {}.
-Instance: Params (@st_E) 3 := {}.
-Instance: Params (@st_own) 3 := {}.
+Global Existing Instance st_own_persistent.
+Global Instance: Params (@st_size) 3 := {}.
+Global Instance: Params (@st_lfts) 3 := {}.
+Global Instance: Params (@st_E) 3 := {}.
+Global Instance: Params (@st_own) 3 := {}.
 Arguments st_size {_ _ _} _ / : simpl nomatch.
 Arguments st_lfts {_ _ _} _ / : simpl nomatch.
 Arguments st_E {_ _ _} _ / : simpl nomatch.
@@ -227,9 +227,9 @@ Record plain_type `{!typeG Σ} 𝔄 := {
   pt_own_persistent v tid vl : Persistent (pt_own v tid vl);
   pt_size_eq v tid vl : pt_own v tid vl -∗ ⌜length vl = pt_size⌝;
 }.
-Existing Instance pt_own_persistent.
-Instance: Params (@pt_size) 3 := {}.
-Instance: Params (@pt_own) 3 := {}.
+Global Existing Instance pt_own_persistent.
+Global Instance: Params (@pt_size) 3 := {}.
+Global Instance: Params (@pt_own) 3 := {}.
 Arguments pt_size {_ _ _} _ / : simpl nomatch.
 Arguments pt_own {_ _ _} _ _ _ _ / : simpl nomatch.
 
@@ -264,13 +264,13 @@ Section ofe.
     (∀vπ d tid vs, ty.(ty_own) vπ d tid vs ≡ ty'.(ty_own) vπ d tid vs) →
     (∀vπ d κ tid l, ty.(ty_shr) vπ d κ tid l ≡ ty'.(ty_shr) vπ d κ tid l) →
     type_equiv' ty ty'.
-  Instance type_equiv {𝔄} : Equiv (type 𝔄) := type_equiv'.
+  Global Instance type_equiv {𝔄} : Equiv (type 𝔄) := type_equiv'.
   Inductive type_dist' {𝔄} (n: nat) (ty ty': type 𝔄) : Prop := TypeDist:
     ty.(ty_size) = ty'.(ty_size) → ty.(ty_lfts) = ty'.(ty_lfts) → ty.(ty_E) = ty'.(ty_E) →
     (∀vπ d tid vs, ty.(ty_own) vπ d tid vs ≡{n}≡ ty'.(ty_own) vπ d tid vs) →
     (∀vπ d κ tid l, ty.(ty_shr) vπ d κ tid l ≡{n}≡ ty'.(ty_shr) vπ d κ tid l) →
     type_dist' n ty ty'.
-  Instance type_dist {𝔄} : Dist (type 𝔄) := type_dist'.
+  Global Instance type_dist {𝔄} : Dist (type 𝔄) := type_dist'.
 
   Definition type_unpack {𝔄} (ty: type 𝔄)
     : prodO (prodO (prodO (prodO natO (listO lftO)) (listO (prodO lftO lftO)))
@@ -368,13 +368,13 @@ Section ofe_lemmas.
     st.(st_size) = st'.(st_size) → st.(st_lfts) = st'.(st_lfts) → st.(st_E) = st'.(st_E) →
     (∀vπ d tid vl, st.(st_own) vπ d tid vl ≡ st'.(st_own) vπ d tid vl) →
     simple_type_equiv' st st'.
-  Instance simple_type_equiv {𝔄} : Equiv (simple_type 𝔄) := simple_type_equiv'.
+  Global Instance simple_type_equiv {𝔄} : Equiv (simple_type 𝔄) := simple_type_equiv'.
   Inductive simple_type_dist' {𝔄} (n: nat) (st st': simple_type 𝔄) : Prop :=
     SimpleTypeDist:
     st.(st_size) = st'.(st_size) → st.(st_lfts) = st'.(st_lfts) → st.(st_E) = st'.(st_E) →
     (∀vπ d tid vl, st.(st_own) vπ d tid vl ≡{n}≡ (st'.(st_own) vπ d tid vl)) →
     simple_type_dist' n st st'.
-  Instance simple_type_dist {𝔄} : Dist (simple_type 𝔄) := simple_type_dist'.
+  Global Instance simple_type_dist {𝔄} : Dist (simple_type 𝔄) := simple_type_dist'.
 
   Definition simple_type_ofe_mixin {𝔄} : OfeMixin (simple_type 𝔄).
   Proof.
@@ -406,12 +406,12 @@ Section ofe_lemmas.
     pt.(pt_size) = pt'.(pt_size) →
     (∀v tid vl, pt.(pt_own) v tid vl ≡ pt'.(pt_own) v tid vl) →
     plain_type_equiv' pt pt'.
-  Instance plain_type_equiv {𝔄} : Equiv (plain_type 𝔄) := plain_type_equiv'.
+  Global Instance plain_type_equiv {𝔄} : Equiv (plain_type 𝔄) := plain_type_equiv'.
   Inductive plain_type_dist' {𝔄} (n: nat) (pt pt': plain_type 𝔄) : Prop := PlainTypeDist:
     pt.(pt_size) = pt'.(pt_size) →
     (∀v tid vl, pt.(pt_own) v tid vl ≡{n}≡ (pt'.(pt_own) v tid vl)) →
     plain_type_dist' n pt pt'.
-  Instance plain_type_dist {𝔄} : Dist (plain_type 𝔄) := plain_type_dist'.
+  Global Instance plain_type_dist {𝔄} : Dist (plain_type 𝔄) := plain_type_dist'.
 
   Definition plain_type_unpack {𝔄} (pt: plain_type 𝔄)
     : prodO natO (𝔄 -d> thread_id -d> list val -d> iPropO Σ) :=
@@ -662,22 +662,22 @@ Class Copy `{!typeG Σ} {𝔄} (ty: type 𝔄) := {
       (na_own tid (F ∖ shr_locsE l ty.(ty_size)) -∗ l ↦∗{q'} vl
         ={E}=∗ na_own tid F ∗ q.[κ])
 }.
-Existing Instances copy_persistent.
-Instance: Params (@Copy) 3 := {}.
+Global Existing Instance copy_persistent.
+Global Instance: Params (@Copy) 3 := {}.
 
 Notation ListCopy := (TCHForall (λ 𝔄, @Copy _ _ 𝔄)).
 
 Class Send `{!typeG Σ} {𝔄} (ty: type 𝔄) :=
   send_change_tid tid tid' vπ d vl :
     ty.(ty_own) vπ d tid vl ⊣⊢ ty.(ty_own) vπ d tid' vl.
-Instance: Params (@Send) 3 := {}.
+Global Instance: Params (@Send) 3 := {}.
 
 Notation ListSend := (TCHForall (λ 𝔄, @Send _ _ 𝔄)).
 
 Class Sync `{!typeG Σ} {𝔄} (ty: type 𝔄) :=
   sync_change_tid tid tid' vπ d κ l :
     ty.(ty_shr) vπ d κ tid l ⊣⊢ ty.(ty_shr) vπ d κ tid' l.
-Instance: Params (@Sync) 3 := {}.
+Global Instance: Params (@Sync) 3 := {}.
 
 Notation ListSync := (TCHForall (λ 𝔄, @Sync _ _ 𝔄)).
 
@@ -758,7 +758,7 @@ Definition resolve `{!typeG Σ} {𝔄} (E: elctx) (L: llctx) (ty: type 𝔄) (Φ
   ∀F qL vπ d tid vl, ↑lftN ∪ ↑prophN ⊆ F →
     lft_ctx -∗ proph_ctx -∗ elctx_interp E -∗ llctx_interp L qL -∗
     ty.(ty_own) vπ d tid vl ={F}=∗ |={F}▷=>^d |={F}=> ⟨π, Φ (vπ π)⟩ ∗ llctx_interp L qL.
-Instance: Params (@resolve) 3 := {}.
+Global Instance: Params (@resolve) 3 := {}.
 
 Definition resolvel `{!typeG Σ} {𝔄l} (E: elctx) (L: llctx) (tyl: typel 𝔄l)
                  (Φl: plist (λ 𝔄, 𝔄 → Prop) 𝔄l) : Prop :=
@@ -870,15 +870,15 @@ Definition type_incl `{!typeG Σ} {𝔄 𝔅} (ty: type 𝔄) (ty': type 𝔅) (
   ⌜ty.(ty_size) = ty'.(ty_size)⌝ ∗ (ty_lft ty' ⊑ ty_lft ty) ∗
   (□ ∀vπ d tid vl, ty.(ty_own) vπ d tid vl -∗ ty'.(ty_own) (f ∘ vπ) d tid vl) ∗
   (□ ∀vπ d κ tid l, ty.(ty_shr) vπ d κ tid l -∗ ty'.(ty_shr) (f ∘ vπ) d κ tid l).
-Instance: Params (@type_incl) 4 := {}.
+Global Instance: Params (@type_incl) 4 := {}.
 
 Definition subtype `{!typeG Σ} {𝔄 𝔅} E L (ty: type 𝔄) (ty': type 𝔅) (f: 𝔄 → 𝔅)
   : Prop := ∀qL, llctx_interp L qL -∗ □ (elctx_interp E -∗ type_incl ty ty' f).
-Instance: Params (@subtype) 6 := {}.
+Global Instance: Params (@subtype) 6 := {}.
 
 Definition eqtype `{!typeG Σ} {𝔄 𝔅} E L (ty: type 𝔄) (ty': type 𝔅)
   (f: 𝔄 → 𝔅) (g: 𝔅 → 𝔄) : Prop := subtype E L ty ty' f ∧ subtype E L ty' ty g.
-Instance: Params (@eqtype) 6 := {}.
+Global Instance: Params (@eqtype) 6 := {}.
 
 Definition subtype_id `{!typeG Σ} {𝔄} E L (ty ty': type 𝔄) : Prop
   := subtype E L ty ty' id.
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index a643d732..e1da9699 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -23,10 +23,10 @@ Notation predl 𝔄l := (pred' (plist of_syn_type 𝔄l)).
 Notation predl_trans 𝔄l 𝔅l := (predl 𝔅l → predl 𝔄l).
 Notation predl_trans' 𝔄l 𝔅 := (pred' 𝔅 → predl 𝔄l).
 
-Instance pred'_equiv A : Equiv (pred' A) := pointwise_relation _ (↔).
-Instance predl_trans_equiv 𝔄l 𝔅l : Equiv (predl_trans 𝔄l 𝔅l) :=
+Global Instance pred'_equiv A : Equiv (pred' A) := pointwise_relation _ (↔).
+Global Instance predl_trans_equiv 𝔄l 𝔅l : Equiv (predl_trans 𝔄l 𝔅l) :=
   pointwise_relation _ (pointwise_relation _ (↔)).
-Instance predl_trans'_equiv 𝔄l 𝔅 : Equiv (predl_trans' 𝔄l 𝔅) :=
+Global Instance predl_trans'_equiv 𝔄l 𝔅 : Equiv (predl_trans' 𝔄l 𝔅) :=
   pointwise_relation _ (pointwise_relation _ (↔)).
 
 Notation predₛ 𝔄 := (𝔄 → Propₛ)%ST.
@@ -37,7 +37,7 @@ Definition trans_app {𝔄l 𝔅l ℭl 𝔇l} (tr: predl_trans 𝔄l 𝔅l) (tr'
   : predl_trans (𝔄l ++ ℭl) (𝔅l ++ 𝔇l) := λ post acl,
   let '(al, cl) := psep acl in tr (λ bl, tr' (λ dl, post (bl -++ dl)) cl) al.
 
-Instance trans_app_proper {𝔄l 𝔅l ℭl 𝔇l} tr tr' :
+Global Instance trans_app_proper {𝔄l 𝔅l ℭl 𝔇l} tr tr' :
   Proper ((≡) ==> (≡)) tr →
   Proper ((≡) ==> (≡)) tr' →
   Proper ((≡) ==> (≡)) (@trans_app 𝔄l 𝔅l ℭl 𝔇l tr tr').
diff --git a/theories/util/basic.v b/theories/util/basic.v
index 2249a47e..d9f8ec7d 100644
--- a/theories/util/basic.v
+++ b/theories/util/basic.v
@@ -27,7 +27,7 @@ Proof. done. Qed.
 Definition s_comb {A B C} (f: A → B → C) (g: A → B) x := (f x) (g x).
 Infix "⊛" := s_comb (left associativity, at level 50).
 Global Arguments s_comb {_ _ _} _ _ _ / : assert.
-Typeclasses Transparent s_comb.
+Global Typeclasses Transparent s_comb.
 
 Class Inj3 {A B C D} (R1: relation A) (R2: relation B) (R3: relation C)
     (S: relation D) (f: A → B → C → D) : Prop :=
diff --git a/theories/util/fancy_lists.v b/theories/util/fancy_lists.v
index 2f09d759..5be053ea 100644
--- a/theories/util/fancy_lists.v
+++ b/theories/util/fancy_lists.v
@@ -538,13 +538,13 @@ End Forall.
 Section HForallTwo.
 Context {A} {F: A → Type} {Xl: list A} (R: ∀X, F X → F X → Prop).
 
-Instance HForallTwo_reflexive :
+Global Instance HForallTwo_reflexive :
   (∀X, Reflexive (R X)) → Reflexive (HForallTwo R (Xl:=Xl)).
 Proof. move=> ?. elim; by constructor. Qed.
-Instance HForallTwo_symmetric :
+Global Instance HForallTwo_symmetric :
   (∀X, Symmetric (R X)) → Symmetric (HForallTwo R (Xl:=Xl)).
 Proof. move=> >. elim; by constructor. Qed.
-Instance HForallTwo_transitive :
+Global Instance HForallTwo_transitive :
   (∀X, Transitive (R X)) → Transitive (HForallTwo R (Xl:=Xl)).
 Proof.
   move=> ??? zl All. move: zl. elim: All; [done|]=> > ?? IH ? All.
@@ -561,8 +561,8 @@ End HForallTwo.
 Section hlist_ofe.
 Context {A} {F: A → ofe} {Xl: list A}.
 
-Instance hlist_equiv : Equiv (hlist F Xl) := HForallTwo (λ _, (≡)).
-Instance hlist_dist : Dist (hlist F Xl) := λ n, HForallTwo (λ _, dist n).
+Global Instance hlist_equiv : Equiv (hlist F Xl) := HForallTwo (λ _, (≡)).
+Global Instance hlist_dist : Dist (hlist F Xl) := λ n, HForallTwo (λ _, dist n).
 
 Definition hlist_ofe_mixin : OfeMixin (hlist F Xl).
 Proof.
-- 
GitLab