diff options
Diffstat (limited to 'doc/sphinx/credits.rst')
-rw-r--r-- | doc/sphinx/credits.rst | 13 |
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 | |