From 2c2e2af0659615c373aba8db82119e5eeba1bb49 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 15 Mar 2018 17:34:48 +0100
Subject: Fix some items in Credits

---
 doc/sphinx/credits.rst | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'doc')

diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst
index b4d816f9f3..ad7b8c4463 100644
--- a/doc/sphinx/credits.rst
+++ b/doc/sphinx/credits.rst
@@ -1309,10 +1309,7 @@ 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.
-
-- Gallina: always use the projection printing style for primitive
-  projections by Maxime Dénès.
+  still does not accept evars) by Pierre-Marie Pédrot.
 
 - Notations: many improvements on recursive notations and
   integration with pattern binding by Hugo Herbelin.
-- 
cgit v1.2.3


From fee3f7413a96a10ec2ac24f51b21d13a0838891f Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 16 Mar 2018 10:10:33 -0300
Subject: Latest fixes.

I think we can all agree this release has a chilean flavor anyway (as in
hot and cold :)
---
 doc/sphinx/credits.rst | 13 ++++---------
 1 file changed, 4 insertions(+), 9 deletions(-)

(limited to 'doc')

diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst
index ad7b8c4463..a60f326454 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
 |
-- 
cgit v1.2.3