diff --git a/theories/bi/lib/counterexamples.v b/theories/bi/lib/counterexamples.v
index 029e1cffc7426a35a14ea6ca2bbcb98dc0f0f32a..83c02d18f16de1df588cf49b93b2bbfb614a5503 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.