From b9ba53329f76426c7037ff53421a1fd4f4e73bda Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 6 Feb 2020 14:53:56 +0100
Subject: [PATCH] typo and gamma

---
 theories/bi/lib/counterexamples.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/bi/lib/counterexamples.v b/theories/bi/lib/counterexamples.v
index 029e1cffc..83c02d18f 100644
--- a/theories/bi/lib/counterexamples.v
+++ b/theories/bi/lib/counterexamples.v
@@ -271,7 +271,7 @@ End linear1. End linear1.
 
 (** This proves that if we have linear impredicative invariants, we can still
 drop arbitrary resources (i.e., we can "defeat" linearity).
-Variant 2: the invariant can depend on the chose gname, and we also have
+Variant 2: the invariant can depend on the chosen [Î³], and we also have
 an accessor that gives back the invariant token immediately,
 not just after the invariant got closed again. *)
 Module linear2. Section linear2.
-- 
GitLab