From 632f92c5f017df0f30bdbf11371929017dabdcf5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 20 May 2021 09:16:41 +0000
Subject: [PATCH] fix typo

---
 docs/proof_guide.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docs/proof_guide.md b/docs/proof_guide.md
index 59ab9118a..5e4e60348 100644
--- a/docs/proof_guide.md
+++ b/docs/proof_guide.md
@@ -216,7 +216,7 @@ For details, consult [the Coq manual](https://coq.inria.fr/refman/user-extension
 * UR: unital cameras or resources algebras
 * F: functors (can be combined with all of the above, e.g. OF is an OFE functor)
 * G: global camera functor management (typeclass; see the [resource algebra docs](resource_algebras.md))
-* GS: global singleton (a `*G` typeclass withe extra data that needs to be unique in a proof)
+* GS: global singleton (a `*G` type class with extra data that needs to be unique in a proof)
 * GpreS: collecting preconditions to instantiate the corresponding `*GS`
 * I: bunched implication logic (of type `bi`)
 * SI: step-indexed bunched implication logic (of type `sbi`)
-- 
GitLab