diff --git a/docs/proof_guide.md b/docs/proof_guide.md
index 5e4e603488b713b3e55b9088b6e3144a914eecf8..1da235b8b184ed35cff232603e18960a2c356900 100644
--- a/docs/proof_guide.md
+++ b/docs/proof_guide.md
@@ -99,9 +99,10 @@ for further details on `libG` classes).  For example, the STS library is
 parameterized by an STS and assumes that the STS state space is inhabited:
 ```coq
 Class stsG Σ (sts : stsT) := {
-  sts_inG :> inG Σ (stsR sts);
+  sts_inG : inG Σ (stsR sts);
   sts_inhabited :> Inhabited (sts.state sts);
 }.
+Local Existing Instance sts_inG.
 ```
 In this case, the `Instance` for this `libG` class has more than just a `subG`
 assumption:
diff --git a/docs/resource_algebras.md b/docs/resource_algebras.md
index 3fc047bf5f2991fcf657b351ad865d3fe4ff3163..1c32b743b8b2789d8d6ac2d6295465497dcb9a8a 100644
--- a/docs/resource_algebras.md
+++ b/docs/resource_algebras.md
@@ -14,7 +14,8 @@ Libraries typically bundle the `inG` they need in a `libG` typeclass, so they do
 not have to expose to clients what exactly their resource algebras are. For
 example, in the [one-shot example](../tests/one_shot.v), we have:
 ```coq
-Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
+Class one_shotG Σ := { one_shot_inG : inG Σ one_shotR }.
+Local Existing Instance one_shot_inG.
 ```
 The `:>` means that the projection `one_shot_inG` is automatically registered as
 an instance for type-class resolution.  If you need several resource algebras,
@@ -273,8 +274,9 @@ Putting it all together, the `libG` typeclass and `libΣ` list of functors for
 your example would look as follows:
 
 ```coq
-Class libG Σ := { lib_inG :> inG Σ (gmapR K (agreeR (prodO natO (laterO (iPropO Σ))))) }.
+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.
 Instance subG_libΣ {Σ} : subG libΣ Σ → libG Σ.
 Proof. solve_inG. Qed.
 ```