Latest fixes.

I think we can all agree this release has a chilean flavor anyway (as in
hot and cold :)

1 files changed, 4 insertions, 9 deletions

diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst
index ad7b8c446..a60f32645 100644
--- a/doc/sphinx/credits.rst
+++ b/doc/sphinx/credits.rst
@@ -1311,8 +1311,8 @@ with a few new features. The main user visible changes are:
   for CIC, by Matthieu Sozeau. Handling of evars in the VM (the kernel
   still does not accept evars) by Pierre-Marie Pédrot.
 
-- 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 ``{``
@@ -1366,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
@@ -1401,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
 |