Merge branch 'master' into ltac2-hooks

1 files changed, 11 insertions, 1 deletions

diff --git a/CHANGES b/CHANGES
index 60b88ea8db..b5f6ba9279 100644
--- a/CHANGES
+++ b/CHANGES
@@ -17,7 +17,17 @@ 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.
+
+Vernacular Commands
+
+- Goals context can be printed in a more compact way when "Set
+  Printing Compact Contexts" is activated.
+
 
 Standard Library