Merge branch 'trunk' into located_switch

1 files changed, 13 insertions, 1 deletions

diff --git a/CHANGES b/CHANGES
index 60b88ea8db..31d691be0e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -17,7 +17,19 @@ 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.
+
+- The deprecated `Save` vernacular and its form `Save Theorem id` to
+  close proofs have been removed from the syntax. Please use `Qed`.
 
 Standard Library