From f3cb208d3172d0726e18f45a03d0a18dee2b4743 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 21 Feb 2019 13:00:00 +0100
Subject: update CHANGES

---
 CHANGES.md | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/CHANGES.md b/CHANGES.md
index c309002beb..e02de0224e 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -48,6 +48,13 @@ Kernel
 
 - Added primitive integers
 
+- Unfolding heuristic in termination checking made more complete.
+  In particular Coq is now more aggressive in unfolding constants
+  when it looks for a iota redex. Performance regression may occur
+  in Fixpoint declarations without an explicit {struct} annotation,
+  since guessing the decreasing argument can now be more expensive.
+  (PR #9602)
+
 Notations
 
 - New command `Declare Scope` to explicitly declare a scope name
-- 
cgit v1.2.3