Mention guard condition in CHANGES.

1 files changed, 5 insertions, 0 deletions

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