diff --git a/theories/examples/folly_queue/refinement.v b/theories/examples/folly_queue/refinement.v
index e083cf80ed2c0a6f1c6ea9faa0186befb9cddc4b..432f59da6eb877d863b59a773dc5f8f32d0e761f 100644
--- a/theories/examples/folly_queue/refinement.v
+++ b/theories/examples/folly_queue/refinement.v
@@ -28,11 +28,11 @@ Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations.
 (* Begin hooks to make `lia` work with Nat.modulo and Nat.div *)
 Require Import Arith ZArith ZifyClasses ZifyInst Lia.
 
-Program Instance Op_Nat_mod : BinOp Nat.modulo :=
+Global Program Instance Op_Nat_mod : BinOp Nat.modulo :=
   {| TBOp := Z.modulo ; TBOpInj := Nat2Z_inj_mod |}.
 Add Zify BinOp Op_Nat_mod.
 
-Program Instance Op_Nat_div : BinOp Nat.div :=
+Global Program Instance Op_Nat_div : BinOp Nat.div :=
   {| TBOp := Z.div ; TBOpInj := Nat2Z_inj_div |}.
 Add Zify BinOp Op_Nat_div.
 
@@ -250,7 +250,7 @@ Section queue_refinement.
   (* Given the total number of push or pop operations that has been carried out,
   ops, returns the number of operations that has affected the i'th SEQ/TS. *)
   Definition nr_of_affecting_ops (q i ops : nat) :=
-    (ops / q) + (if i <? ops `mod` q then 1 else 0).
+    (ops / q) + (if i <? ops `mod` q then 1 else 0)%nat.
 
   (* Helper lemmas *)
   Lemma mod_S_le a b :
@@ -293,7 +293,7 @@ Section queue_refinement.
   Proof.
     unfold nr_of_affecting_ops.
     rewrite div0 mod0.
-    assert (i <? 0 = false) as ->.
+    assert (i <? 0 = false)%nat as ->.
     { apply Nat.ltb_nlt. lia. }
     done.
   Qed.
@@ -319,7 +319,7 @@ Section queue_refinement.
         cut (ops `div` q = (ops + 1) `div` q)%Z; first lia.
         eapply (Zdiv_unique _ _ _ (ops `mod` q + 1)); first lia.
         rewrite {1}Hops2. lia.
-      + assert (i <? (ops + 1) `mod` q = false) as ->.
+      + assert (i <? (ops + 1) `mod` q = false)%nat as ->.
         { by apply Nat.ltb_nlt. }
         rewrite Nat.add_0_r.
         destruct (decide ((ops + 1) `mod` q ≤ ops `mod` q)) as [Hsucc|Hsucc]; last lia.
@@ -329,7 +329,7 @@ Section queue_refinement.
         { lia. }
         cut (ops `div` q + 1 = (ops + 1) `div` q)%Z ; first lia.
         eapply (Zdiv_unique _ _ _ 0); lia.
-    - assert (i <? ops `mod` q = false) as ->.
+    - assert (i <? ops `mod` q = false)%nat as ->.
       { by apply Nat.ltb_nlt. }
       rewrite Nat.add_0_r.
       destruct (decide (i < (ops + 1) `mod` q)) as [Hops3|Hops3].
@@ -338,7 +338,7 @@ Section queue_refinement.
         cut (ops `div` q = (ops + 1) `div` q)%Z; first lia.
         eapply (Zdiv_unique _ _ _ (ops `mod` q + 1)); first lia.
         rewrite {1}Hops2. lia.
-      + assert (i <? (ops+1) `mod` q = false) as ->.
+      + assert (i <? (ops+1) `mod` q = false)%nat as ->.
         { by apply Nat.ltb_nlt. }
         rewrite Nat.add_0_r.
         cut (ops `div` q = (ops + 1) `div` q)%Z; first lia.
@@ -358,7 +358,7 @@ Section queue_refinement.
   Proof.
     intros Hgt Heq. symmetry.
     rewrite /nr_of_affecting_ops.
-    assert (i <? ops `mod` q = false) as ->.
+    assert (i <? ops `mod` q = false)%nat as ->.
     { apply Nat.ltb_ge. lia. }
     rewrite Nat.add_0_r.
     assert (Z.of_nat ops = (q * (ops `div` q)%Z + i%Z)%Z)%Z as Hops2.
@@ -371,7 +371,7 @@ Section queue_refinement.
       eapply (Zdiv_unique _ _ _ (i+1)); first lia.
       rewrite {1}Hops2. lia.
     - assert ((ops + 1) `mod` q ≤ i) by lia.
-      assert (i <? (ops + 1) `mod` q = false) as ->.
+      assert (i <? (ops + 1) `mod` q = false)%nat as ->.
       { by apply Nat.ltb_ge. }
       rewrite Nat.add_0_r.
       cut (((ops `div` q) + 1) = (ops + 1) `div` q)%Z; first lia.
@@ -436,7 +436,7 @@ Section queue_refinement.
     rewrite /turn_ctx. iFrame "He".
     rewrite (nr_of_affecting_ops_incr_eq q _ popT); [|lia|lia].
     rewrite /nr_of_affecting_ops.
-    assert (_ <? _ = false) as ->.
+    assert (_ <? _ = false)%nat as ->.
     { apply Nat.ltb_ge. lia. }
     autorewrite with natb.
     by rewrite dequeue_turns_take.
@@ -452,7 +452,7 @@ Section queue_refinement.
     rewrite /turn_ctx. iFrame "Hd".
     rewrite (nr_of_affecting_ops_incr_eq q _ pushT); try lia.
     rewrite /nr_of_affecting_ops.
-    assert (_ <? _ = false) as ->.
+    assert (_ <? _ = false)%nat as ->.
     { apply Nat.ltb_ge. lia. }
     autorewrite with natb.
     by rewrite enqueue_turns_take.
diff --git a/theories/examples/folly_queue/set.v b/theories/examples/folly_queue/set.v
index bfdd78735f1b9f02c63b3106075f751bed4f1c5f..07fbcfd6a132bdd52a0c05cf6ffbbcb9a2f2b328 100644
--- a/theories/examples/folly_queue/set.v
+++ b/theories/examples/folly_queue/set.v
@@ -83,25 +83,25 @@ Proof.
 Qed.
 
 (* Rewrite n <? m when true *)
-Hint Rewrite ltb_lt_1 using lia : natb.
-Hint Rewrite leb_correct_conv using lia : natb.
-Hint Rewrite leb_correct using lia : natb.
-Hint Rewrite set_above_lookup using lia : natb.
-Hint Rewrite @decide_False using lia : natb.
-Hint Rewrite @decide_True using lia : natb.
-Hint Rewrite set_above_lookup_none using lia : natb.
-Hint Rewrite set_upto_lookup_none using lia : natb.
-Hint Rewrite set_upto_lookup using lia : natb.
-Hint Rewrite set_singleton_lookup_none using lia : natb.
-Hint Rewrite set_singleton_lookup using lia : natb.
-Hint Rewrite div_mod' : natb.
-Hint Rewrite mod0 : natb.
-Hint Rewrite div0 : natb.
-Hint Rewrite Nat.add_0_r : natb.
-Hint Rewrite Nat.add_0_l : natb.
-Hint Rewrite Nat.ltb_irrefl : natb.
-Hint Rewrite Nat.max_0_r : natb.
-Hint Rewrite Nat.max_0_l : natb.
+Global Hint Rewrite ltb_lt_1 using lia : natb.
+Global Hint Rewrite leb_correct_conv using lia : natb.
+Global Hint Rewrite leb_correct using lia : natb.
+Global Hint Rewrite set_above_lookup using lia : natb.
+Global Hint Rewrite @decide_False using lia : natb.
+Global Hint Rewrite @decide_True using lia : natb.
+Global Hint Rewrite set_above_lookup_none using lia : natb.
+Global Hint Rewrite set_upto_lookup_none using lia : natb.
+Global Hint Rewrite set_upto_lookup using lia : natb.
+Global Hint Rewrite set_singleton_lookup_none using lia : natb.
+Global Hint Rewrite set_singleton_lookup using lia : natb.
+Global Hint Rewrite div_mod' : natb.
+Global Hint Rewrite mod0 : natb.
+Global Hint Rewrite div0 : natb.
+Global Hint Rewrite Nat.add_0_r : natb.
+Global Hint Rewrite Nat.add_0_l : natb.
+Global Hint Rewrite Nat.ltb_irrefl : natb.
+Global Hint Rewrite Nat.max_0_r : natb.
+Global Hint Rewrite Nat.max_0_l : natb.
 
 Lemma set_upto_singleton_valid n m : ✓ (set_upto n ⋅ set_singleton m) → n ≤ m.
 Proof.
diff --git a/theories/examples/stack/CG_stack.v b/theories/examples/stack/CG_stack.v
index 9bfb5ac02254dcaf49dcaddbdbd2860107d20d9b..949350e8711131e4ad9e544957f51c556545b0b6 100644
--- a/theories/examples/stack/CG_stack.v
+++ b/theories/examples/stack/CG_stack.v
@@ -42,7 +42,7 @@ Fixpoint val_of_list (ls : list val) : val :=
   | v::vs => CONSV v (val_of_list vs)
   end.
 
-Instance val_to_list_inj : Inj (=@{list val}) (=@{val}) val_of_list.
+Global Instance val_to_list_inj : Inj (=@{list val}) (=@{val}) val_of_list.
 Proof.
   intros ls1. induction ls1 as [|h1 ls1]=>ls2; destruct ls2; naive_solver.
 Qed.
diff --git a/theories/examples/stack_helping/offers.v b/theories/examples/stack_helping/offers.v
index 9ba03c8510ceb667ccfdaed81ff6705831087905..a14a9af862332b3175698b93b75121e95452d669 100644
--- a/theories/examples/stack_helping/offers.v
+++ b/theories/examples/stack_helping/offers.v
@@ -15,7 +15,7 @@ Definition take_offer : val :=
 Definition offerR := exclR unitR.
 Class offerG Σ := { offer_inG :> inG Σ offerR }.
 Definition offerΣ : gFunctors := #[GFunctor offerR].
-Instance subG_offerΣ {Σ} : subG offerΣ Σ → offerG Σ.
+Global Instance subG_offerΣ {Σ} : subG offerΣ Σ → offerG Σ.
 Proof. solve_inG. Qed.
 
 Section rules.
diff --git a/theories/examples/symbol.v b/theories/examples/symbol.v
index a05b387bde08b6163b0a91613271bc7f43c49247..1be89905e174d2f2fcde970f228b37fcd2c6089c 100644
--- a/theories/examples/symbol.v
+++ b/theories/examples/symbol.v
@@ -49,7 +49,7 @@ Definition symbol2 : val := λ: <>,
 Class msizeG Σ := MSizeG { msize_inG :> inG Σ (authR max_natUR) }.
 Definition msizeΣ : gFunctors := #[GFunctor (authR max_natUR)].
 
-Instance subG_msizeΣ {Σ} : subG msizeΣ Σ → msizeG Σ.
+Global Instance subG_msizeΣ {Σ} : subG msizeΣ Σ → msizeG Σ.
 Proof. solve_inG. Qed.
 
 Section rules.
diff --git a/theories/examples/various.v b/theories/examples/various.v
index 48db6e77209d1f3df3c08b79b78cea3dd04da5af..9d9899d36529ddb2c04db6bf53820e8ce819b399 100644
--- a/theories/examples/various.v
+++ b/theories/examples/various.v
@@ -10,7 +10,7 @@ From reloc.lib Require Export lock counter Y.
 Definition oneshotR := csumR (exclR unitR) (agreeR unitR).
 Class oneshotG Σ := { oneshot_inG :> inG Σ oneshotR }.
 Definition oneshotΣ : gFunctors := #[GFunctor oneshotR].
-Instance subG_oneshotΣ {Σ} : subG oneshotΣ Σ → oneshotG Σ.
+Global Instance subG_oneshotΣ {Σ} : subG oneshotΣ Σ → oneshotG Σ.
 Proof. solve_inG. Qed.
 
 Section proofs.
diff --git a/theories/experimental/hocap/counter.v b/theories/experimental/hocap/counter.v
index 2a39ef46fe1f0cfdaab771d41b56b376c10398dd..50635d12eeb73cce924a3291a0c8efbfcc2f413e 100644
--- a/theories/experimental/hocap/counter.v
+++ b/theories/experimental/hocap/counter.v
@@ -11,7 +11,7 @@ Class cnt_hocapG Σ := CntG {
 
 Definition cnt_hocapΣ := GFunctor (authR (optionUR (prodR fracR (agreeR natO)))).
 
-Instance sub_cnt {Σ} : subG cnt_hocapΣ Σ → cnt_hocapG Σ.
+Global Instance sub_cnt {Σ} : subG cnt_hocapΣ Σ → cnt_hocapG Σ.
 Proof. solve_inG. Qed.
 
 Section cnt_model.
diff --git a/theories/lib/lock.v b/theories/lib/lock.v
index caf20f26cc8d0e217033c52f15f1a026cf31dbec..713ff9475719533d55f9c1317f4bd9dec77975d9 100644
--- a/theories/lib/lock.v
+++ b/theories/lib/lock.v
@@ -18,7 +18,7 @@ Definition with_lock : val := λ: "e" "l" "x",
 Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitO) }.
 Definition lockΣ : gFunctors := #[GFunctor (exclR unitO)].
 
-Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
+Global Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
 Proof. solve_inG. Qed.
 
 Section lockG_rules.
diff --git a/theories/logic/adequacy.v b/theories/logic/adequacy.v
index f1ec69944c9fb94d2e0788c8d5c5a9d92ae8806b..0bddd0758964129c1bbaf15cb02960ecffa0c9c8 100644
--- a/theories/logic/adequacy.v
+++ b/theories/logic/adequacy.v
@@ -11,7 +11,7 @@ Class relocPreG Σ := RelocPreG {
 }.
 
 Definition relocΣ : gFunctors := #[heapΣ; GFunctor (authR cfgUR)].
-Instance subG_relocPreG {Σ} : subG relocΣ Σ → relocPreG Σ.
+Global Instance subG_relocPreG {Σ} : subG relocΣ Σ → relocPreG Σ.
 Proof. solve_inG. Qed.
 
 Lemma refines_adequate Σ `{relocPreG Σ}
diff --git a/theories/logic/model.v b/theories/logic/model.v
index 18e244aa3ee093a294229eab9d8b229238a18bf1..0dac2d5ea523a6854adc667f68c175c0434be917 100644
--- a/theories/logic/model.v
+++ b/theories/logic/model.v
@@ -20,7 +20,7 @@ Arguments lrel_car {_} _ _ _ : simpl never.
 Declare Scope lrel_scope.
 Bind Scope lrel_scope with lrel.
 Delimit Scope lrel_scope with lrel.
-Existing Instance lrel_persistent.
+Global Existing Instance lrel_persistent.
 
 (* The COFE structure on semantic types *)
 Section lrel_ofe.
diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index 41f8227cc508648d3791e5ec048c2cc5375b1ef1..c0e14c00a2a497c67118b2b847afcb645cfcf3e0 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -59,7 +59,7 @@ Section definitionsS.
   Global Instance spec_ctx_persistent : Persistent spec_ctx.
   Proof. apply _. Qed.
 End definitionsS.
-Typeclasses Opaque heapS_mapsto tpool_mapsto spec_ctx.
+Global Typeclasses Opaque heapS_mapsto tpool_mapsto spec_ctx.
 
 Notation "l ↦ₛ{ q } v" := (heapS_mapsto l q v)
   (at level 20, q at level 50, format "l  ↦ₛ{ q }  v") : bi_scope.
diff --git a/theories/prelude/lang_facts.v b/theories/prelude/lang_facts.v
index 4c4bbd68d61a87c7c643d0a3d1a2418308a0b71a..334324374d631f357f1c8cff46dad6efa0648a51 100644
--- a/theories/prelude/lang_facts.v
+++ b/theories/prelude/lang_facts.v
@@ -170,7 +170,7 @@ Section facts.
       + specialize (IH h1 Hpure (t1 ++ e3 :: t2 ++ efs) eq_refl eq_refl).
         etrans; last by apply IH.
         eapply rtc_once. econstructor.
-        eapply step_atomic with (t3:=(e2::t1)) (efs0:=efs); eauto.
+        by eapply (step_atomic _ _ _ _ efs (e2::t1)).
   Qed.
 
   Lemma pure_exec_inversion_lemma tp1 tp2 e1 e2 σ1 σ2 v ϕ :
diff --git a/theories/typing/contextual_refinement.v b/theories/typing/contextual_refinement.v
index fb1e21f01c5c3dea3720e8488f2a263c6a6c3d38..3e23b9348702fe97faf06513e4b5eca9668dec4a 100644
--- a/theories/typing/contextual_refinement.v
+++ b/theories/typing/contextual_refinement.v
@@ -262,14 +262,14 @@ Lemma typed_ctx_typed K Γ τ Γ' τ' e :
   typed Γ e τ → typed_ctx K Γ τ Γ' τ' → typed Γ' (fill_ctx K e) τ'.
 Proof. induction 2; simpl; eauto using typed_ctx_item_typed. Qed.
 
-Instance ctx_refines_reflexive Γ τ :
+Global Instance ctx_refines_reflexive Γ τ :
   Reflexive (fun e1 e2 => ctx_refines Γ e1 e2 τ).
 Proof.
   intros e K thp ? σ b Hty Hst.
   eexists _,_. apply Hst.
 Qed.
 
-Instance ctx_refines_transitive Γ τ :
+Global Instance ctx_refines_transitive Γ τ :
   Transitive (fun e1 e2 => ctx_refines Γ e1 e2 τ).
 Proof.
   intros e1 e2 e3 Hctx1 Hctx2 K thp σ₀ σ₁ b Hty Hst.
diff --git a/theories/typing/types.v b/theories/typing/types.v
index 3e90a84046c30ff0526291b13c3c519a1bf85791..01abeb40aa11cb2718aeae8df55305800527a0b6 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -39,10 +39,10 @@ Lemma unboxed_type_ref_or_eqtype Ï„ :
 Proof. inversion 1; first [ left; by econstructor | right; naive_solver ]. Qed.
 
 (** Autosubst instances *)
-Instance Ids_type : Ids type. derive. Defined.
-Instance Rename_type : Rename type. derive. Defined.
-Instance Subst_type : Subst type. derive. Defined.
-Instance SubstLemmas_typer : SubstLemmas type. derive. Qed.
+Global Instance Ids_type : Ids type. derive. Defined.
+Global Instance Rename_type : Rename type. derive. Defined.
+Global Instance Subst_type : Subst type. derive. Defined.
+Global Instance SubstLemmas_typer : SubstLemmas type. derive. Qed.
 
 Definition binop_nat_res_type (op : bin_op) : option type :=
   match op with
@@ -113,7 +113,7 @@ Notation "'unpack:' x := e1 'in' e2" := (unpack e1%E (LamV x%binder e2%E))
   (at level 200, x at level 1, e1, e2 at level 200, only parsing) : val_scope.
 
 (** Operation lifts *)
-Instance insert_binder (A : Type): Insert binder A (stringmap A) :=
+Global Instance insert_binder (A : Type): Insert binder A (stringmap A) :=
   binder_insert.
 
 (** Typing itself *)