diff --git a/Makefile.coq.local b/Makefile.coq.local
new file mode 100644
index 0000000000000000000000000000000000000000..1c985e350e51ee4d99750771412f12a2fe46709d
--- /dev/null
+++ b/Makefile.coq.local
@@ -0,0 +1,11 @@
+# Run tests interleaved with main build.  They have to be in the same target for this.
+real-all: style
+
+style: $(VFILES) coq-lint.sh
+# Make sure everything imports the options, and all Instance/Argument/Hint are qualified.
+	$(SHOW)"COQLINT"
+	$(HIDE)for FILE in $(VFILES); do \
+	  if ! fgrep -q 'From iris.prelude Require Import options.' "$$FILE"; then echo "ERROR: $$FILE does not import 'options'."; echo; exit 1; fi ; \
+	  ./coq-lint.sh "$$FILE" || exit 1; \
+	done
+.PHONY: style
diff --git a/coq-lint.sh b/coq-lint.sh
new file mode 100755
index 0000000000000000000000000000000000000000..3bdadfbb7452374cf668411fa1caacd0c66f6352
--- /dev/null
+++ b/coq-lint.sh
@@ -0,0 +1,12 @@
+#!/bin/bash
+set -e
+## A simple shell script checking for some common Coq issues.
+
+FILE="$1"
+
+if egrep -n '^\s*((Existing\s+|Program\s+|Declare\s+|)Instance|Arguments|Remove|Hint\s+(Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold)|(Open|Close)\s+Scope|Opaque|Transparent)\b' "$FILE"; then
+    echo "ERROR: $FILE contains 'Instance'/'Arguments'/'Hint' or another side-effect without locality (see above)."
+    echo "Please add 'Global' or 'Local' as appropriate."
+    echo
+    exit 1
+fi
diff --git a/theories/lang/adequacy.v b/theories/lang/adequacy.v
index 5f41bde0a3b108b63aa6b610293dcd57f48bcea0..ec4b64cdbbca5c7e96f1724655acd00dc795a529 100644
--- a/theories/lang/adequacy.v
+++ b/theories/lang/adequacy.v
@@ -14,7 +14,7 @@ Definition lrustΣ : gFunctors :=
   #[invΣ;
     GFunctor (constRF (authR heapUR));
     GFunctor (constRF (authR heap_freeableUR))].
-Instance subG_lrustGpreS {Σ} : subG lrustΣ Σ → lrustGpreS Σ.
+Global Instance subG_lrustGpreS {Σ} : 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 2638b7c7b1d94d49629c1032b3cb15081071a25e..db57e30a44decec20b6581a9a8803e5d44a5aa49 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -67,8 +67,8 @@ Section definitions.
 End definitions.
 
 Typeclasses Opaque heap_mapsto heap_freeable heap_mapsto_vec.
-Instance: Params (@heap_mapsto) 4 := {}.
-Instance: Params (@heap_freeable) 5 := {}.
+Global Instance: Params (@heap_mapsto) 4 := {}.
+Global Instance: Params (@heap_freeable) 5 := {}.
 
 Notation "l ↦{ q } v" := (heap_mapsto l q v)
   (at level 20, q at level 50, format "l  ↦{ q }  v") : bi_scope.
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index 0a8dc2732a0ad9fc9e046ad375c4dd2bb295733c..ab1bb8adfb35c3757da19263b07814a6485e70d8 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -59,9 +59,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 :=
@@ -347,10 +347,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 :
@@ -404,7 +404,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.
@@ -548,11 +548,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 :=
@@ -597,17 +597,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 846d97bd7916c90944ecb9cc32525a0b8c441206..055bce8036a073521f85eac79e94b60d056ca730 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -110,7 +110,7 @@ Definition arc_stR :=
 Class arcG Σ :=
   RcG :> inG Σ (authR arc_stR).
 Definition arcΣ : gFunctors := #[GFunctor (authR arc_stR)].
-Instance subG_arcΣ {Σ} : subG arcΣ Σ → arcG Σ.
+Global Instance subG_arcΣ {Σ} : subG arcΣ Σ → arcG Σ.
 Proof. solve_inG. Qed.
 
 Section def.
@@ -161,7 +161,7 @@ Section arc.
   Context `{!lrustGS Σ, !arcG Σ} (P1 : Qp → iProp Σ) {HP1:Fractional P1}
           (P2 : iProp Σ) (N : namespace).
 
-  Instance P1_AsFractional q : AsFractional (P1 q) P1 q.
+  Local Instance P1_AsFractional q : AsFractional (P1 q) P1 q.
   Proof using HP1. done. Qed.
 
   Global Instance arc_inv_ne n :
diff --git a/theories/lang/lib/spawn.v b/theories/lang/lib/spawn.v
index 4dd4154c48a94bad2bcd64f2124410d5d0791782..2b120455906f2de2139a45388dcbc9e9bb284e73 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. *)
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index 997ba3f1b3f2c7056870fd48e7b30dfb4571098f..2b39093d24a9834c6686d4d0e88d9e95016f2769 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -11,7 +11,7 @@ Class lrustGS Σ := LRustGS {
   lrustGS_heapGS :> heapGS Σ
 }.
 
-Instance lrustGS_irisGS `{!lrustGS Σ} : irisGS lrust_lang Σ := {
+Global Instance lrustGS_irisGS `{!lrustGS Σ} : irisGS lrust_lang Σ := {
   iris_invGS := lrustGS_invGS;
   state_interp σ _ κs _ := heap_ctx σ;
   fork_post _ := True%I;
@@ -39,8 +39,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.
 
@@ -51,13 +51,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/lifetime/lifetime.v b/theories/lifetime/lifetime.v
index 27874643b5a80a1503e9fa4e3679e36d79436fb7..3cf40a6b37181579878657292d0b1f7a0025bb5b 100644
--- a/theories/lifetime/lifetime.v
+++ b/theories/lifetime/lifetime.v
@@ -18,7 +18,7 @@ End lifetime.
 
 Notation lft_intersect_list l := (foldr (⊓) static l).
 
-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 c179f0fae97cfe12f928559b647d1ec0332e6f98..134e2ba15b9794509ae0a82b978d4a00067450e0 100644
--- a/theories/lifetime/lifetime_sig.v
+++ b/theories/lifetime/lifetime_sig.v
@@ -23,7 +23,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 Σ userE}, iProp Σ.
 
diff --git a/theories/lifetime/meta.v b/theories/lifetime/meta.v
index 8a535061797e0784fa765582c42d76423efeb3a7..80ebbcc790f5f79cd1b6bddc58e10ddd5e67f992 100644
--- a/theories/lifetime/meta.v
+++ b/theories/lifetime/meta.v
@@ -11,7 +11,7 @@ Class lft_metaG Σ := LftMetaG {
 }.
 Definition lft_metaΣ : gFunctors :=
   #[GFunctor (dyn_reservation_mapR (agreeR gnameO))].
-Instance subG_lft_meta Σ :
+Global Instance subG_lft_meta Σ :
   subG (lft_metaΣ) Σ → lft_metaG Σ.
 Proof. solve_inG. Qed.
 
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index 6c5c38b4e2271178bb6bfdbe288ee13a59d1bcbf..418e1a9159fbb5b931540acf618b352996cf9ef7 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -66,7 +66,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.
 
@@ -200,12 +200,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.
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 140b4d733675cbb7d2a9dce6fe01eae4c9fa1613..080794f6fe89d5aa17cf01836008d7429655fb9d 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 (⊓) := _.
+Local Instance lft_inhabited : Inhabited lft := _.
+Local Instance bor_idx_inhabited : Inhabited bor_idx := _.
+Local Instance lft_intersect_comm : Comm (A:=lft) eq (⊓) := _.
+Local Instance lft_intersect_assoc : Assoc (A:=lft) eq (⊓) := _.
+Local Instance lft_intersect_inj_1 κ : Inj eq eq (κ ⊓.) := _.
+Local Instance lft_intersect_inj_2 κ : Inj eq eq (.⊓ κ) := _.
+Local Instance lft_intersect_left_id : LeftId eq static (⊓) := _.
+Local 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/typing/function.v b/theories/typing/function.v
index 514d37fc9c515c503c9888044e3a5baca768813a..4111d6e4738ba92393b769259a873ee7b74f32ef 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -113,7 +113,7 @@ Section fn.
   Qed.
 End fn.
 
-Arguments fn_params {_ _} _.
+Global Arguments fn_params {_ _} _.
 
 (* We use recursive notation for binders as well, to allow patterns
    like '(a, b) to be used. In practice, only one binder is ever used,
@@ -139,7 +139,7 @@ Notation "'fn(' E ')' '→' R" :=
   (at level 99, R at level 200,
    format "'fn(' E ')'  '→'  R") : lrust_type_scope.
 
-Instance elctx_empty : Empty (lft → elctx) := λ ϝ, [].
+Global Instance elctx_empty : Empty (lft → elctx) := λ ϝ, [].
 
 Section typing.
   Context `{!typeGS Σ}.
diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index fd97c8266ccdf889cb9dcfb069f2aac199ec37ec..40f82bf10f5a62b1ae9ebafd8ae731cac4992517 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -406,14 +406,14 @@ Section lft_contexts.
   Proof. iIntros (??) "_ !> ?". done. Qed.
 End lft_contexts.
 
-Arguments lctx_lft_incl {_ _} _ _ _ _.
-Arguments lctx_lft_eq {_ _} _ _ _ _.
-Arguments lctx_lft_alive {_ _ _} _ _ _.
-Arguments elctx_sat {_ _} _ _ _.
-Arguments lctx_lft_incl_incl {_ _ _ _ _} _ _.
-Arguments lctx_lft_incl_incl_noend {_ _ _ _} _ _.
-Arguments lctx_lft_alive_tok {_ _ _ _ _} _ _ _.
-Arguments lctx_lft_alive_tok_noend {_ _ _ _ _} _ _ _.
+Global Arguments lctx_lft_incl {_ _} _ _ _ _.
+Global Arguments lctx_lft_eq {_ _} _ _ _ _.
+Global Arguments lctx_lft_alive {_ _ _} _ _ _.
+Global Arguments elctx_sat {_ _} _ _ _.
+Global Arguments lctx_lft_incl_incl {_ _ _ _ _} _ _.
+Global Arguments lctx_lft_incl_incl_noend {_ _ _ _} _ _.
+Global Arguments lctx_lft_alive_tok {_ _ _ _ _} _ _ _.
+Global Arguments lctx_lft_alive_tok_noend {_ _ _ _ _} _ _ _.
 
 Lemma elctx_sat_submseteq `{!invGS Σ, !lftGS Σ lft_userE} E E' L :
   E' ⊆+ E → elctx_sat E L E'.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 1c818641835b1daa1ce9f72f5f4c047bfc36f94b..865d1692c7fb5c33ba9cdc669e58aeeec1c1dc08 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 ν).
+  Local 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/brandedvec.v b/theories/typing/lib/brandedvec.v
index ef673b5aa8bfa12e9c8bca8265a971d9da199bfd..1a104e7780fcaf5703d187e51f8e8b9bf3148f2d 100644
--- a/theories/typing/lib/brandedvec.v
+++ b/theories/typing/lib/brandedvec.v
@@ -14,7 +14,7 @@ Class brandidxG Σ := BrandedIdxG {
 
 Definition brandidxΣ : gFunctors
   := #[GFunctor (authR brandidx_stR); lft_metaΣ].
-Instance subG_brandidxΣ {Σ} : subG brandidxΣ Σ → brandidxG Σ.
+Global Instance subG_brandidxΣ {Σ} : subG brandidxΣ Σ → brandidxG Σ.
 Proof. solve_inG. Qed.
 
 Definition brandidxN := lrustN .@ "brandix".
diff --git a/theories/typing/lib/ghostcell.v b/theories/typing/lib/ghostcell.v
index 6ff1ae07f6566d2ca4e36fcf8d4cda3d0b670ce6..0caa82fe4ba949e1b977f621c41f1dbe625412fd 100644
--- a/theories/typing/lib/ghostcell.v
+++ b/theories/typing/lib/ghostcell.v
@@ -76,7 +76,7 @@ Class ghostcellG Σ := GhostcellG {
 Definition ghostcellΣ : gFunctors
   := #[GFunctor ghosttoken_stR ; lft_metaΣ].
 
-Instance subG_ghostcellΣ {Σ} : subG ghostcellΣ Σ → ghostcellG Σ.
+Global Instance subG_ghostcellΣ {Σ} : subG ghostcellΣ Σ → ghostcellG Σ.
 Proof. solve_inG. Qed.
 
 (* There are two possible states:
@@ -375,8 +375,6 @@ Section ghostcell.
     eqtype E L (ghostcell κ1 ty1) (ghostcell κ2 ty2).
   Proof. intros. by apply ghostcell_proper. Qed.
 
-  Hint Resolve ghostcell_mono' ghostcell_proper' : lrust_typing.
-
   Global Instance ghostcell_send α ty :
     Send ty → Send (ghostcell α ty).
   Proof. by unfold ghostcell, Send. Qed.
@@ -753,3 +751,5 @@ Section ghostcell.
   Qed.
 
 End ghostcell.
+
+Global Hint Resolve ghostcell_mono' ghostcell_proper' : lrust_typing.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 1c186f39a4256e7377d7490ef26a730ac22432e8..a597e9b3c0a50be09c023f5e0ebcf62ae3cefd5c 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 e081d0179a37eb391a6e303b5fa376e8cd192396..f50434c7f378d07daf8805ab4d85929214c0b1a7 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 5df708e4dabb016cc45a68dd893bf5e97e5fa695..f211296ce0bdb0e160d23289b9f00ceac16c4fda 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/own.v b/theories/typing/own.v
index 05911b2421258bd76c0c1d500923c6d64d778c51..abf06d116e957d8f606826c673f4cfb681a4cce3 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -13,7 +13,7 @@ Section own.
     | _, 0%nat => False
     | sz, n => †{pos_to_Qp (Pos.of_nat sz) / pos_to_Qp (Pos.of_nat n)}l…sz
     end%I.
-  Arguments freeable_sz : simpl never.
+  Global Arguments freeable_sz : simpl never.
 
   Global Instance freeable_sz_timeless n sz l : Timeless (freeable_sz n sz l).
   Proof. destruct sz, n; apply _. Qed.
diff --git a/theories/typing/product.v b/theories/typing/product.v
index cea73ac8dd0b0f2f8e327c21be3ca38224c98c8e..701bfc65b119e9e488f9f3074d7a34650763a495 100644
--- a/theories/typing/product.v
+++ b/theories/typing/product.v
@@ -263,7 +263,7 @@ Section typing.
   Qed.
 End typing.
 
-Arguments product : simpl never.
+Global Arguments product : simpl never.
 Global Hint Opaque product : lrust_typing lrust_typing_merge.
 Global Hint Resolve product_mono' product_proper' ty_outlives_E_elctx_sat_product
   : lrust_typing.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index c4692f28c4fe860972f9b0c1875c5ebc1eadf2fc..abc8515b205240c53f41d7ad394853afd658a14e 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -104,11 +104,11 @@ End typing.
 Definition typed_instruction_ty `{!typeGS Σ} (E : elctx) (L : llctx) (T : tctx)
     (e : expr) (ty : type) : iProp Σ :=
   typed_instruction E L T e (λ v, [v ◁ ty]).
-Arguments typed_instruction_ty {_ _} _ _ _ _%E _%T.
+Global Arguments typed_instruction_ty {_ _} _ _ _ _%E _%T.
 
 Definition typed_val `{!typeGS Σ} (v : val) (ty : type) : Prop :=
   ∀ E L, ⊢ typed_instruction_ty E L [] (of_val v) ty.
-Arguments typed_val _ _ _%V _%T.
+Global Arguments typed_val _ _ _%V _%T.
 
 Section typing_rules.
   Context `{!typeGS Σ}.
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index 294469f01a825d9d3d9f6217e3e0ee3db2452776..a2623b755f341576851f8d20c9d39b94633a0246 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -16,7 +16,7 @@ Class typeGpreS Σ := PreTypeG {
 
 Definition typeΣ : gFunctors :=
   #[lrustΣ; lftΣ; na_invΣ; GFunctor (constRF fracR)].
-Instance subG_typeGpreS {Σ} : subG typeΣ Σ → typeGpreS Σ.
+Global Instance subG_typeGpreS {Σ} : subG typeΣ Σ → typeGpreS Σ.
 Proof. solve_inG. Qed.
 
 Section type_soundness.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index 5c78ab2c2d684283fa1b1aa09ee10b7135ac1e7f..f197ac8104c5b008ce833089cc021bd8d84973dc 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -50,11 +50,11 @@ Global Instance: Params (@ty_size) 2 := {}.
 Global Instance: Params (@ty_own) 2 := {}.
 Global Instance: Params (@ty_shr) 2 := {}.
 
-Arguments ty_own {_ _} !_ _ _ / : simpl nomatch.
+Global Arguments ty_own {_ _} !_ _ _ / : simpl nomatch.
 
 Class TyWf `{!typeGS Σ} (ty : type) := { ty_lfts : list lft; ty_wf_E : elctx }.
-Arguments ty_lfts {_ _} _ {_}.
-Arguments ty_wf_E {_ _} _ {_}.
+Global Arguments ty_lfts {_ _} _ {_}.
+Global Arguments ty_wf_E {_ _} _ {_}.
 
 Definition ty_outlives_E `{!typeGS Σ} ty `{!TyWf ty} (κ : lft) : elctx :=
   (λ α, κ ⊑ₑ α) <$> (ty_lfts ty).
@@ -77,7 +77,7 @@ Inductive ListTyWf `{!typeGS Σ} : list type → Type :=
 | list_ty_wf_nil : ListTyWf []
 | list_ty_wf_cons ty tyl `{!TyWf ty, !ListTyWf tyl} : ListTyWf (ty::tyl).
 Existing Class ListTyWf.
-Existing Instances list_ty_wf_nil list_ty_wf_cons.
+Global Existing Instances list_ty_wf_nil list_ty_wf_cons.
 
 Fixpoint tyl_lfts `{!typeGS Σ} tyl {WF : ListTyWf tyl} : list lft :=
   match WF with
@@ -117,7 +117,7 @@ Record simple_type `{!typeGS Σ} :=
     st_size_eq tid vl : st_own tid vl -∗ ⌜length vl = 1%nat⌝;
     st_own_persistent tid vl : Persistent (st_own tid vl) }.
 Global Existing Instance st_own_persistent.
-Instance: Params (@st_own) 2 := {}.
+Global Instance: Params (@st_own) 2 := {}.
 
 Program Definition ty_of_st `{!typeGS Σ} (st : simple_type) : type :=
   {| ty_size := 1; ty_own := st.(st_own);
@@ -157,14 +157,14 @@ Section ofe.
       (∀ tid vs, ty1.(ty_own) tid vs ≡ ty2.(ty_own) tid vs) →
       (∀ κ tid l, ty1.(ty_shr) κ tid l ≡ ty2.(ty_shr) κ tid l) →
       type_equiv' ty1 ty2.
-  Instance type_equiv : Equiv type := type_equiv'.
+  Local Instance type_equiv : Equiv type := type_equiv'.
   Inductive type_dist' (n : nat) (ty1 ty2 : type) : Prop :=
     Type_dist :
       ty1.(ty_size) = ty2.(ty_size) →
       (∀ tid vs, ty1.(ty_own) tid vs ≡{n}≡ ty2.(ty_own) tid vs) →
       (∀ κ tid l, ty1.(ty_shr) κ tid l ≡{n}≡ ty2.(ty_shr) κ tid l) →
       type_dist' n ty1 ty2.
-  Instance type_dist : Dist type := type_dist'.
+  Local Instance type_dist : Dist type := type_dist'.
 
   Let T := prodO
     (prodO natO (thread_id -d> list val -d> iPropO Σ))
@@ -225,12 +225,12 @@ Section ofe.
     St_equiv :
       (∀ tid vs, ty1.(ty_own) tid vs ≡ ty2.(ty_own) tid vs) →
       st_equiv' ty1 ty2.
-  Instance st_equiv : Equiv simple_type := st_equiv'.
+  Local Instance st_equiv : Equiv simple_type := st_equiv'.
   Inductive st_dist' (n : nat) (ty1 ty2 : simple_type) : Prop :=
     St_dist :
       (∀ tid vs, ty1.(ty_own) tid vs ≡{n}≡ (ty2.(ty_own) tid vs)) →
       st_dist' n ty1 ty2.
-  Instance st_dist : Dist simple_type := st_dist'.
+  Local Instance st_dist : Dist simple_type := st_dist'.
 
   Definition st_unpack (ty : simple_type) : thread_id -d> list val -d> iPropO Σ :=
     λ tid vl, ty.(ty_own) tid vl.
@@ -399,31 +399,31 @@ Class Copy `{!typeGS Σ} (t : type) := {
       (na_own tid (F ∖ shr_locsE l t.(ty_size)) -∗ ▷l ↦∗{q'}: t.(ty_own) tid
                                   ={E}=∗ na_own tid F ∗ q.[κ])
 }.
-Existing Instances copy_persistent.
-Instance: Params (@Copy) 2 := {}.
+Global Existing Instances copy_persistent.
+Global Instance: Params (@Copy) 2 := {}.
 
 Class ListCopy `{!typeGS Σ} (tys : list type) := lst_copy : Forall Copy tys.
-Instance: Params (@ListCopy) 2 := {}.
+Global Instance: Params (@ListCopy) 2 := {}.
 Global Instance lst_copy_nil `{!typeGS Σ} : ListCopy [] := List.Forall_nil _.
 Global Instance lst_copy_cons `{!typeGS Σ} ty tys :
   Copy ty → ListCopy tys → ListCopy (ty :: tys) := List.Forall_cons _ _ _.
 
 Class Send `{!typeGS Σ} (t : type) :=
   send_change_tid tid1 tid2 vl : t.(ty_own) tid1 vl -∗ t.(ty_own) tid2 vl.
-Instance: Params (@Send) 2 := {}.
+Global Instance: Params (@Send) 2 := {}.
 
 Class ListSend `{!typeGS Σ} (tys : list type) := lst_send : Forall Send tys.
-Instance: Params (@ListSend) 2 := {}.
+Global Instance: Params (@ListSend) 2 := {}.
 Global Instance lst_send_nil `{!typeGS Σ} : ListSend [] := List.Forall_nil _.
 Global Instance lst_send_cons `{!typeGS Σ} ty tys :
   Send ty → ListSend tys → ListSend (ty :: tys) := List.Forall_cons _ _ _.
 
 Class Sync `{!typeGS Σ} (t : type) :=
   sync_change_tid κ tid1 tid2 l : t.(ty_shr) κ tid1 l -∗ t.(ty_shr) κ tid2 l.
-Instance: Params (@Sync) 2 := {}.
+Global Instance: Params (@Sync) 2 := {}.
 
 Class ListSync `{!typeGS Σ} (tys : list type) := lst_sync : Forall Sync tys.
-Instance: Params (@ListSync) 2 := {}.
+Global Instance: Params (@ListSync) 2 := {}.
 Global Instance lst_sync_nil `{!typeGS Σ} : ListSync [] := List.Forall_nil _.
 Global Instance lst_sync_cons `{!typeGS Σ} ty tys :
   Sync ty → ListSync tys → ListSync (ty :: tys) := List.Forall_cons _ _ _.
@@ -536,23 +536,23 @@ Definition type_incl `{!typeGS Σ} (ty1 ty2 : type) : iProp Σ :=
     (⌜ty1.(ty_size) = ty2.(ty_size)⌝ ∗
      (□ ∀ tid vl, ty1.(ty_own) tid vl -∗ ty2.(ty_own) tid vl) ∗
      (□ ∀ κ tid l, ty1.(ty_shr) κ tid l -∗ ty2.(ty_shr) κ tid l))%I.
-Instance: Params (@type_incl) 2 := {}.
+Global Instance: Params (@type_incl) 2 := {}.
 (* Typeclasses Opaque type_incl. *)
 
 Definition type_equal `{!typeGS Σ} (ty1 ty2 : type) : iProp Σ :=
     (⌜ty1.(ty_size) = ty2.(ty_size)⌝ ∗
      (□ ∀ tid vl, ty1.(ty_own) tid vl ∗-∗ ty2.(ty_own) tid vl) ∗
      (□ ∀ κ tid l, ty1.(ty_shr) κ tid l ∗-∗ ty2.(ty_shr) κ tid l))%I.
-Instance: Params (@type_equal) 2 := {}.
+Global Instance: Params (@type_equal) 2 := {}.
 
 Definition subtype `{!typeGS Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
   ∀ qmax qL, llctx_interp_noend qmax L qL -∗ □ (elctx_interp E -∗ type_incl ty1 ty2).
-Instance: Params (@subtype) 4 := {}.
+Global Instance: Params (@subtype) 4 := {}.
 
 (* TODO: The prelude should have a symmetric closure. *)
 Definition eqtype `{!typeGS Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
   subtype E L ty1 ty2 ∧ subtype E L ty2 ty1.
-Instance: Params (@eqtype) 4 := {}.
+Global Instance: Params (@eqtype) 4 := {}.
 
 Section subtyping.
   Context `{!typeGS Σ}.