From 1411b0a97e458656b548644418f13cb932ca77f4 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Mon, 21 Mar 2022 00:26:24 +0000
Subject: [PATCH] Only use Existing Instances.

---
 docs/resource_algebras.md | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/docs/resource_algebras.md b/docs/resource_algebras.md
index eed48bbf6..71d547b32 100644
--- a/docs/resource_algebras.md
+++ b/docs/resource_algebras.md
@@ -15,12 +15,13 @@ 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 }.
-Local Existing Instance one_shot_inG.
+Local Existing Instances one_shot_inG.
 ```
 Here, the projection `one_shot_inG` is registered as an instance for type-class
 resolution. If you need several resource algebras, just add more `inG` fields.
 If you are using another module as part of yours, add a field like
-`one_shot_other : otherG Σ`. All of these fields should be added to the `Local Existing Instances`.
+`one_shot_other : otherG Σ`. All of these fields should be added to the
+`Local Existing Instances` command.
 
 The code above enables these typeclass instances only in the surrounding file
 where they are used to define the new abstractions by the library. The
@@ -132,7 +133,7 @@ Class gen_heapGS (L V : Type) (Σ : gFunctors) `{Countable L} := GenHeapGS {
   gen_heap_inG : gen_heapGpreS L V Σ;
   gen_heap_name : gname;
 }.
-Local Existing Instance gen_heap_inG.
+Local Existing Instances gen_heap_inG.
 ```
 The trailing `S` here is for "singleton", because the idea is that only one
 instance of `gen_heapGS` ever exists. This is important, since two instances
-- 
GitLab