aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/sphinx/credits.rst
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-04-11 12:38:03 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-04-11 16:20:36 +0200
commit912659dd84b8e8975523cb39eb291b70e2486287 (patch)
tree83e463191314f1f3168c81fd1587d2d3a2d8dedd /doc/sphinx/credits.rst
parent75df94937d7832926ea979718fb0a8fdb44f3e1a (diff)
Add credits related to the Sphinx migration.
Closes #7209.
Diffstat (limited to 'doc/sphinx/credits.rst')
-rw-r--r--doc/sphinx/credits.rst9
1 files changed, 8 insertions, 1 deletions
diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst
index 8a396014c..f3d9f57b4 100644
--- a/doc/sphinx/credits.rst
+++ b/doc/sphinx/credits.rst
@@ -1338,7 +1338,14 @@ with a few new features. The main user visible changes are:
- Documentation: a large community effort resulted in the migration
of the reference manual to the Sphinx documentation tool. The result
- is this manual.
+ is this manual. The new documentation infrastructure (based on Sphinx)
+ is by Clément Pit-Claudel. The migration was coordinated by Maxime Dénès
+ and Paul Steckler, with some help of Théo Zimmermann during the
+ final integration phase. The 14 people who ported the manual are
+ Calvin Beck, Heiko Becker, Yves Bertot, Maxime Dénès, Richard Ford,
+ Pierre Letouzey, Assia Mahboubi, Clément Pit-Claudel,
+ Laurence Rideau, Matthieu Sozeau, Paul Steckler, Enrico Tassi,
+ Laurent Théry, Nikita Zyuzin.
- Tools: experimental ``-mangle-names`` option to coqtop/coqc for
linting proof scripts, by Jasper Hugunin.