From 4e28d88de719711a608389a02f9358182eec5235 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 16 Mar 2021 11:48:57 +0100
Subject: Typo in ChoiceFacts.

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

diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 3dac62c476..23bc396fd7 100644
--- a/theories/Logic/ChoiceFacts.v
+++ b/theories/Logic/ChoiceFacts.v
@@ -676,7 +676,7 @@ Qed.
 
     We show instead that functional relation reification and the
     functional form of the axiom of choice are equivalent on decidable
-    relation with [nat] as codomain
+    relations with [nat] as codomain.
 *)
 
 Require Import Wf_nat.
-- 
cgit v1.2.3