aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMatthieu Sozeau2016-11-06 11:22:31 +0100
committerMatthieu Sozeau2016-11-06 11:43:50 +0100
commitceaafcde70e0ba536cae03baa740563aff47f6e8 (patch)
treedc3bbb34b1bc45eeec40693994c2c7aa7bc25bf1
parent25fc9919c6d86fa8119b1f0c8e5ddba156055c9d (diff)
Maxime's comments
-rw-r--r--doc/refman/RefMan-pre.tex36
1 files changed, 20 insertions, 16 deletions
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 669ba11e81..944cd48481 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -1087,7 +1087,7 @@ Paris, January 2015, revised December 2015,\\
Hugo Herbelin, Matthieu Sozeau and the {\Coq} development team\\
\end{flushright}
-\section*{Credits: version 8.6 (Stronger, Better, Faster Rooster)}
+\section*{Credits: version 8.6}
{\Coq} version 8.6 contains the result of refinements, stabilization of
8.5's features and cleanups of the internals of the system. Over the
@@ -1098,7 +1098,8 @@ over 100 contributions integrated. The main user visible changes are:
can outperform the previous version by an order of magnitude, by
Jacques-Henri Jourdan.
\item In CoqIDE and other asynchronous interfaces, more fine-grained
- asynchronous processing and error reporting by Enrico Tassi.
+ asynchronous processing and error reporting by Enrico Tassi (ability
+ to jump to any error in the document).
\item More access to the proof engine features from Ltac: goal
management primitives, range selectors and a {\tt typeclasses
eauto} engine handling multiple goals and multiple successes, by
@@ -1170,22 +1171,25 @@ The OPAM repository for {\Coq} packages has been maintained by Guillaume
Claret, Guillaume Melquiond, Matthieu Sozeau, Enrico Tassi and others. A
list of packages is now available at \url{https://coq.inria.fr/opam/www/}.
-Packaging tools and software development kits were prepared by Maxime
-Dénès, Michael Soegtrop and Enrico Tassi for Windows, and Maxime Dénès
-and Matthieu Sozeau for MacOS X. Packages are now regularly built on the
-continuous integration server.
+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 and Matthieu Sozeau for MacOS X. Packages are now regularly
+built on the continuous integration server.
Matej Košík maintained and greatly improved the continuous integration
setup and the testing of {\Coq} contributions. He also contributed many
API improvement and code cleanups throughout the system.
-General maintenance during part or whole of this period has been done by
-Pierre Boutillier, Pierre Courtieu, Maxime Dénès, Hugo Herbelin, Pierre
-Letouzey, Guillaume Melquiond, Pierre-Marie Pédrot, Matthieu Sozeau,
-Arnaud Spiwack, Enrico Tassi, Bruno Barras, Yves Bertot,
-Frédéric Besson, Assia Mahboubi and Yann Régis-Gianas. The development
-process was coordinated by Matthieu Sozeau with the help of Maxime
-Dénès, who was also in charge of the release process.
+The contributors for this version are C.J. Bell, Yves Bertot, Frédéric
+Besson, Tej Chajed, Pierre Courtieu, Maxime Dénès, Ricky Elrod, Jason
+Gross, Hugo Herbelin, Emilio Jesus Gallego Arias, Jacques-Henri Jourdan,
+Matej Košík, Xavier Leroy, Pierre Letouzey, Gregory Malecha, Cyprien
+Mangin, Erik Martin-Dorel, Guillaume Melquiond, Pierre-Marie Pédrot,
+Lionel Rieg, Gabriel Scherer, Matthieu Sozeau, Arnaud Spiwack, Paul
+Steckler, Laurent Théry, Enrico Tassi, Nickolai Zeldovich, Théo
+Zimmermann and Daniel de Rauglaudre. The development process was
+coordinated by Hugo Herbelin and Matthieu Sozeau with the help of
+Maxime Dénès, who was also in charge of the release process.
Many power users helped to improve the design of the new features via
the bug tracker, the pull request system, the {\Coq} development mailing
@@ -1193,8 +1197,8 @@ list or the coq-club mailing list. Special thanks to the users who
contributed patches and intensive brain-storming and code reviews,
starting with Cyril Cohen, Jason Gross, Robbert Krebbers, Jonathan
Leivent, Xavier Leroy, Gregory Malecha, Clément Pit-Claudel, Gabriel
-Sherer and Beta Ziliani. It would however be impossible to mention with
-precision all the names of people who to some extent influenced the
+Sherer and Beta Ziliani. It would however be impossible to mention
+exhaustively the names of everybody who to some extent influenced the
development.
Version 8.6 is the first release of {\Coq} developed on a time-based
@@ -1203,7 +1207,7 @@ development cycle. Its development spanned 10 months from the release of
external contributions than any previous {\Coq} system. Code reviews
were systematically done before integration of new features, with an
important focus given to compatibility and performance issues, resulting
-in a hopefully much more robust release than previous ones.
+in a hopefully more robust release than {\Coq} 8.5.
Coq Enhancement Proposals (CEPs for short) were introduced by Enrico
Tassi to provide more visibility and a discussion period on new