diff --git a/docs/resource_algebras.md b/docs/resource_algebras.md
index 1c32b743b8b2789d8d6ac2d6295465497dcb9a8a..55c472ae6a8d68a33045b0156bd24a5175b8257f 100644
--- a/docs/resource_algebras.md
+++ b/docs/resource_algebras.md
@@ -275,8 +275,9 @@ your example would look as follows:
 
 ```coq
 Class libG Σ := { lib_inG : inG Σ (gmapR K (agreeR (prodO natO (laterO (iPropO Σ))))) }.
-Definition libΣ : gFunctors := #[GFunctor (gmapRF K (agreeRF (natO * ▶ ∙)))].
 Local Existing Instance lib_inG.
+
+Definition libΣ : gFunctors := #[GFunctor (gmapRF K (agreeRF (natO * ▶ ∙)))].
 Instance subG_libΣ {Σ} : subG libΣ Σ → libG Σ.
 Proof. solve_inG. Qed.
 ```
diff --git a/iris/base_logic/lib/cancelable_invariants.v b/iris/base_logic/lib/cancelable_invariants.v
index 2515ed6be324d038f530cb69be7562cdc20f953e..8273c0797a3940270cf051043ae2a403deb5768a 100644
--- a/iris/base_logic/lib/cancelable_invariants.v
+++ b/iris/base_logic/lib/cancelable_invariants.v
@@ -6,9 +6,10 @@ From iris.prelude Require Import options.
 Import uPred.
 
 Class cinvG Σ := cinv_inG : inG Σ fracR.
-Definition cinvΣ : gFunctors := #[GFunctor fracR].
 Local Existing Instance cinv_inG.
 
+Definition cinvΣ : gFunctors := #[GFunctor fracR].
+
 Global Instance subG_cinvΣ {Σ} : subG cinvΣ Σ → cinvG Σ.
 Proof. solve_inG. Qed.
 
diff --git a/iris/base_logic/lib/gset_bij.v b/iris/base_logic/lib/gset_bij.v
index 9be5df415bcd35a60ccec1ba8f21924f155168d4..402144c42b7b012b0eaee2d34521d49ea6dec368 100644
--- a/iris/base_logic/lib/gset_bij.v
+++ b/iris/base_logic/lib/gset_bij.v
@@ -29,8 +29,8 @@ From iris.prelude Require Import options.
 (* The uCMRA we need. *)
 Class gset_bijG Σ A B `{Countable A, Countable B} :=
   GsetBijG { gset_bijG_inG : inG Σ (gset_bijR A B); }.
-Global Hint Mode gset_bijG - ! ! - - - - : typeclass_instances.
 Local Existing Instance gset_bijG_inG.
+Global Hint Mode gset_bijG - ! ! - - - - : typeclass_instances.
 
 Definition gset_bijΣ A B `{Countable A, Countable B}: gFunctors :=
   #[ GFunctor (gset_bijR A B) ].