Add credits related to the Sphinx migration.

Closes #7209.

2 files changed, 9 insertions, 1 deletions

diff --git a/CREDITS b/CREDITS
index 8675b1a64..7d9dfb492 100644
--- a/CREDITS
+++ b/CREDITS
@@ -148,6 +148,7 @@ of the Coq Proof assistant during the indicated time:
   Pierre-Marie Pédrot (INRIA-PPS, 2011-2015, INRIA-Ascola, 2015-2016,
                        University of Ljubljana, 2016-2017,
                        MPI-SWS, 2017-2018)
+  Clément Pit-Claudel (MIT, 2015-2018)
   Matthias Puech (INRIA-Bologna, 2008-2011)
   Yann Régis-Gianas (INRIA-PPS then IRIF, 2009-now)
   Clément Renard (INRIA, 2001-2004)
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.