From cc1212c3cfbd9c39cbe981210758c67cf9095be2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 27 Apr 2017 17:25:14 +0200
Subject: Tentative note in CHANGES about now applying βι while typing "match"
 branches.

In practice, this is almost invisible except when using "refine". So,
in some sense, it is aligning the behavior of pretyping on the one of
logic.ml's "refine" so that the more natural behavior of 8.4's refine
on this issue is restored.
---
 CHANGES | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 60b88ea8db..8cb5573b21 100644
--- a/CHANGES
+++ b/CHANGES
@@ -18,6 +18,11 @@ Tactics
     missed before because of a missing normalization step. Hopefully this should
     be fairly uncommon.
 - "auto with real" can now discharge comparisons of literals
+- The types of variables in patterns of "match" are now
+  beta-iota-reduced after type-checking. This has an impact on the
+  type of the variables that the tactic "refine" introduces in the
+  context, producing types a priori closer to the expectations.
+
 
 Standard Library
 
-- 
cgit v1.2.3


From 06f3ce00971283d2718e272ec9f123430d75ffa6 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Thu, 11 May 2017 15:16:21 +0200
Subject: Documenting Printing Compact Contexts + CHANGES

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

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 60b88ea8db..9318a0df11 100644
--- a/CHANGES
+++ b/CHANGES
@@ -19,6 +19,12 @@ Tactics
     be fairly uncommon.
 - "auto with real" can now discharge comparisons of literals
 
+Vernacular Commands
+
+- Goals context can be printed in a more compact way when "Set
+  Printing Compact Contexts" is activated.
+
+
 Standard Library
 
 - New file PropExtensionality.v to explicitly work in the axiomatic
-- 
cgit v1.2.3


From ba88e99d37817cd3a591b14bbceb61e28f3e3382 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 27 Apr 2017 17:26:17 +0200
Subject: Aligning on standard layout of CHANGES.

---
 CHANGES | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 8cb5573b21..69271f932e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -17,13 +17,12 @@ Tactics
     Most notably, the new implementation recognizes Miller patterns that were
     missed before because of a missing normalization step. Hopefully this should
     be fairly uncommon.
-- "auto with real" can now discharge comparisons of literals
+- Tactic "auto with real" can now discharge comparisons of literals.
 - The types of variables in patterns of "match" are now
   beta-iota-reduced after type-checking. This has an impact on the
   type of the variables that the tactic "refine" introduces in the
   context, producing types a priori closer to the expectations.
 
-
 Standard Library
 
 - New file PropExtensionality.v to explicitly work in the axiomatic
-- 
cgit v1.2.3