From a030dceb0142b707a0ff7b1600f3f4adb9f8a6af Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Tue, 1 Mar 2022 21:53:45 +0100
Subject: [PATCH] Use new style for `inG` instances in docs as well

---
 docs/proof_guide.md       | 3 ++-
 docs/resource_algebras.md | 6 ++++--
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/docs/proof_guide.md b/docs/proof_guide.md
index 5e4e60348..1da235b8b 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 3fc047bf5..1c32b743b 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.
 ```
-- 
GitLab