From 87bdd8c2724cfb865bb7e9782b183e8b65d6997f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 15 Jan 2015 07:50:47 +0100
Subject: Mention guard condition in CHANGES.

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

diff --git a/CHANGES b/CHANGES
index 4a9c3a40d8..2088fa6ff7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -35,6 +35,11 @@ Logic
 - New universe polymorphism.
 - New option -type-in-type to collapse the universe hierarchy (this makes the
   logic inconsistent).
+- The guard condition for fixpoints is now a bit stricter. Propagation of
+subterm value through pattern matching is restricted according to the return
+predicate. Restores compatibility of Coq's logic with the propositional
+extensionality axiom. May create incompatibilities in recursive programs heavily
+using dependent types.
 
 Vernacular commands
 
-- 
cgit v1.2.3