Merge PR #7003: 8.8 changes

2 files changed, 23 insertions, 15 deletions

diff --git a/CHANGES b/CHANGES
index 399e62de5..26f07540a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,5 +1,11 @@
-Changes beyond 8.7
-==================
+Changes from 8.7.2 to 8.8+beta1
+===============================
+
+Kernel
+
+- Support for template polymorphism for definitions was removed. May trigger
+  more "universe inconsistency" errors in rare occasions.
+- Fixpoints are no longer allowed on non-recursive inductive types.
 
 Notations
 
@@ -56,6 +62,8 @@ Tactics
 - Added tactics "assert_succeeds tac" and "assert_fails tac" to ensure
   properties of the executation of a tactic without keeping the effect
   of the execution.
+- `vm_compute` now supports existential variables.
+- Calls to `shelve` and `give_up` within calls to tactic `refine` now working.
 
 Focusing
 
@@ -80,6 +88,9 @@ Vernacular Commands
 - The "Export" modifier can now be used when setting and unsetting options, and
   will result in performing the same change when the module corresponding the
   command is imported.
+- The `Axiom` command does not automatically declare axioms as instances when
+  their type is a class. Previous behavior can be restored using `Set
+  Typeclasses Axioms Are Instances`.
 
 Universes
 
@@ -106,6 +117,7 @@ Tools
   name scheme. This is intended to function as a linter for developments that
   want to be robust to changes in auto-generated names. This feature is experimental,
   and may change or dissapear without warning.
+- GeoProof support was removed.
 
 Checker
 
@@ -127,6 +139,9 @@ Documentation
 - The Coq FAQ, formerly located at https://coq.inria.fr/faq, has been
   moved to the GitHub wiki section of this repository; the main entry
   page is https://github.com/coq/coq/wiki/The-Coq-FAQ.
+- Documentation: a large community effort resulted in the migration
+  of the reference manual to the Sphinx documentation tool. The result
+  is partially integrated in this version.
 
 Standard Library
 
@@ -138,6 +153,7 @@ Standard Library
   positive, N, Z, and string.
 - Added [Coq.Strings.String.concat] to concatenate a list of strings
   inserting a separator between each item
+- Notation `'` for Zpos in QArith was removed.
 
 - Some deprecated aliases are now emitting warnings when used.
 
diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst
index b4d816f9f..a60f32645 100644
--- a/doc/sphinx/credits.rst
+++ b/doc/sphinx/credits.rst
@@ -1309,13 +1309,10 @@ with a few new features. The main user visible changes are:
 - Kernel: fix a subject reduction failure due to allowing fixpoints
   on non-recursive values, which allows to recover full parametricity
   for CIC, by Matthieu Sozeau. Handling of evars in the VM (the kernel
-  still does not accept evars) by Maxime Dénès.
+  still does not accept evars) by Pierre-Marie Pédrot.
 
-- Gallina: always use the projection printing style for primitive
-  projections by Maxime Dénès.
-
-- Notations: many improvements on recursive notations and
-  integration with pattern binding by Hugo Herbelin.
+- Notations: many improvements on recursive notations and support for
+  destructuring patterns in the syntax of notations by Hugo Herbelin.
 
 - Proof language: tacticals for profiling, timing and checking success
   or failure of tactics by Jason Gross. The focusing bracket ``{``
@@ -1369,11 +1366,6 @@ The OPAM repository for |Coq| packages has been maintained by Guillaume
 Melquiond, Matthieu Sozeau, Enrico Tassi with contributions from many
 users. A list of packages is available at https://coq.inria.fr/opam/www.
 
-Packaging tools and software development kits were prepared by Michael
-Soegtrop with the help of Maxime Dénès and Enrico Tassi for Windows, and
-Maxime Dénès for macOS. Packages are regularly built on the
-Travis and GitLab continuous integration server.
-
 The 40 contributors for this version are Yves Bertot, Joachim
 Breitner, Tej Chajed, Arthur Charguéraud, Jacques-Pascal Deplaix, Maxime
 Dénès, Jim Fehrle, Yannick Forster, Gaëtan Gilbert, Jason Gross, Samuel
@@ -1404,6 +1396,6 @@ The |Coq| consortium, an organization directed towards users and
 supporters of the system, is now running and employs Maxime Dénès.
 The contacts of the Coq Consortium are Yves Bertot and Maxime Dénès.
 
-| Paris, March 2018,
-| Matthieu Sozeau and the |Coq| development team
+| Santiago de Chile, March 2018,
+| Matthieu Sozeau for the |Coq| development team
 |