From 248bc07a8db01b57d5965ceb68f3e260f740ea10 Mon Sep 17 00:00:00 2001
From: David Swasey <swasey@mpi-sws.org>
Date: Sun, 23 Feb 2020 12:42:03 +0100
Subject: [PATCH] Rename `cogpick` to `coGpick` (oops).

---
 theories/coGset.v | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/theories/coGset.v b/theories/coGset.v
index 73a06d04..84e93102 100644
--- a/theories/coGset.v
+++ b/theories/coGset.v
@@ -134,13 +134,13 @@ Section infinite.
 End infinite.
 
 (** * Pick elements from infinite sets *)
-Definition cogpick `{Countable A, Infinite A} (X : coGset A) : A :=
+Definition coGpick `{Countable A, Infinite A} (X : coGset A) : A :=
   fresh (match X with FinGSet _ => ∅ | CoFinGset X => X end).
 
-Lemma cogpick_elem_of `{Countable A, Infinite A} X :
-  ¬set_finite X → cogpick X ∈ X.
+Lemma coGpick_elem_of `{Countable A, Infinite A} X :
+  ¬set_finite X → coGpick X ∈ X.
 Proof.
-  unfold cogpick. destruct X as [X|X]; rewrite coGset_finite_spec; simpl.
+  unfold coGpick. destruct X as [X|X]; rewrite coGset_finite_spec; simpl.
   done. by intros _; apply is_fresh.
 Qed.
 
-- 
GitLab