From 9133d6faece4feb675fdc9c66cebcb2bba9246a9 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 3 Mar 2017 14:43:00 +0100
Subject: CHANGES: choice over setoids and prop. ext.

---
 CHANGES | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/CHANGES b/CHANGES
index 4a7cb8c45e..a7cba9aa4f 100644
--- a/CHANGES
+++ b/CHANGES
@@ -7,6 +7,15 @@ Tactics
   functional extensionality in H supposed to be a quantified equality
   until giving a bare equality.
 
+Libraries
+
+- New file PropExtensionality.v to explicitly work in the axiomatic
+  context of propositional extensionality.
+- New file SetoidChoice.v axiomatically providing choice over setoids,
+  and, consequently, choice of representatives in equivalence classes.
+  Various proof-theoretic characterizations of choice over setoids in
+  file ChoiceFacts.v.
+
 Changes from V8.6beta1 to V8.6
 ==============================
 
-- 
cgit v1.2.3