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


From c1e9a27d383688e44ba34ada24fe08151cb5846e Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 17 May 2017 21:04:18 +0200
Subject: [vernac] Remove `Save thm id.` command.

We'd like to cleanup the `proof_end` type so we can have a smaller
path in proof save. Note that the construction:

```
Goal Type.
⋮
Save id.
```

has to be handled by the STM in the same path as Defined (but with an
opaque flag), as `Save id` will alter the environment and cannot be
processed in parallel.

We thus try to simply such paths a bit, as complexity of `lemmas.ml`
seems like an issue these days. The form `Save Theorem id` doesn't
really seem used, and moreover we should really add a type of "Goal",
and unify syntax.

It is often the case that beginners try `Goal addnC n : n + 0 = n."
etc...
---
 CHANGES | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index b5f6ba9279..31d691be0e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -28,6 +28,8 @@ 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
 
-- 
cgit v1.2.3