From 682546592e51552431d4273ad3a4ca8194964d67 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 6 Oct 2014 21:52:26 -0400
Subject: [PATCH] Fix compilation with Coq 8.4pl4.

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

diff --git a/theories/countable.v b/theories/countable.v
index bd621021..6ea46907 100644
--- a/theories/countable.v
+++ b/theories/countable.v
@@ -68,7 +68,7 @@ Lemma surjective_cancel `{Countable A} `{∀ x y : B, Decision (x = y)}
   (f : A → B) `{!Surjective (=) f} : { g : B → A & Cancel (=) f g }.
 Proof.
   exists (λ y, choose (λ x, f x = y) (surjective f y)).
-  intros y. by rewrite (choose_correct _ (surjective f y)).
+  intros y. by rewrite (choose_correct (λ _, _) (surjective f y)).
 Qed.
 
 (** ** Instances *)
-- 
GitLab