Update CREDITS on a best-effort basis.

And with help from https://github.com/coq/coq/graphs/contributors

1 files changed, 30 insertions, 11 deletions

diff --git a/CREDITS b/CREDITS
index c6848648e..95ca5685a 100644
--- a/CREDITS
+++ b/CREDITS
@@ -7,7 +7,10 @@ The "Coq proof assistant" was jointly developed by
   associated to CNRS and university Paris Sud (since Sep. 1997),
 - Laboratoire d'Informatique de l'Ecole Polytechnique (LIX)
   associated to CNRS and Ecole Polytechnique (since Jan. 2003).
-- Laboratoire PPS associated to CNRS and university Paris 7 (since Jan. 2009).
+- Laboratoire PPS associated to CNRS and University Paris Diderot
+  (Jan. 2009 - Dec. 2015).
+- Institut de Recherche en Informatique Fondamentale (IRIF),
+  associated to CNRS and University Paris Diderot (since Jan. 2016).
 
 All files of the "Coq proof assistant" in directories or sub-directories of
 
@@ -15,8 +18,8 @@ All files of the "Coq proof assistant" in directories or sub-directories of
   scripts states tactics test-suite theories tools toplevel
 
 are distributed under the terms of the GNU Lesser General Public License
-Version 2.1 (see file LICENSE). These files are COPYRIGHT 1999-2010,
-The Coq development team, CNRS, INRIA and Université Paris Sud.
+Version 2.1 (see file LICENSE). These files are COPYRIGHT 1999-2017,
+The Coq development team, INRIA, CNRS, LIX, LRI, PPS.
 
 Files from the directory doc are distributed as indicated in file doc/LICENCE.
 
@@ -37,8 +40,8 @@ plugins/firstorder
 plugins/fourier
   developed by Loïc Pottier (INRIA-Lemme, 2001)
 plugins/funind
-  developed by Pierre Courtieu (INRIA-Lemme, 2003-2004, CNAM, 2004-2008),
-  Julien Forest (INRIA-Everest, 2006, CNAM, 2007-2008)
+  developed by Pierre Courtieu (INRIA-Lemme, 2003-2004, CNAM, 2006-now),
+  Julien Forest (INRIA-Everest, 2006, CNAM, 2007-2008, ENSIIE, 2008-now)
   and Yves Bertot (INRIA-Marelle, 2005-2006)
 plugins/omega
   developed by Pierre Crégut (France Telecom R&D, 1996)
@@ -60,7 +63,7 @@ plugins/ssrmatching
 plugins/subtac
   developed by Matthieu Sozeau (LRI, 2005-2008)
 plugins/micromega
-  developed by Frédéric Besson (IRISA/INRIA, 2006-2008), with some
+  developed by Frédéric Besson (IRISA/INRIA, 2006-now), with some
   extensions by Evgeny Makarov (INRIA, 2007); sum-of-squares solver and
   interface to the csdp solver uses code from John Harrison (University
   of Cambridge, 1998)
@@ -94,32 +97,41 @@ of the Coq Proof assistant during the indicated time:
 
   Bruno Barras (INRIA, 1995-now)
   Yves Bertot (INRIA, 2000-now)
-  Pierre Boutillier (INRIA-PPS, 2010-now)
+  Pierre Boutillier (INRIA-PPS, 2010-2015)
   Xavier Clerc (INRIA, 2012-2014)
+  Tej Chajed (MIT, 2016-now)
   Jacek Chrzaszcz (LRI, 1998-2003)
   Thierry Coquand (INRIA, 1985-1989)
   Pierre Corbineau (LRI, 2003-2005, Nijmegen, 2005-2008, Grenoble 1, 2008-2011)
   Cristina Cornes (INRIA, 1993-1996)
   Yann Coscoy (INRIA Sophia-Antipolis, 1995-1996)
+  Pierre Courtieu (CNAM, 2006-now)
   David Delahaye (INRIA, 1997-2002)
   Maxime Dénès (INRIA, 2013-now)
-  Daniel de Rauglaudre (INRIA, 1996-1998)
+  Daniel de Rauglaudre (INRIA, 1996-1998, 2012, 2016)
   Olivier Desmettre (INRIA, 2001-2003)
   Gilles Dowek (INRIA, 1991-1994)
   Amy Felty (INRIA, 1993)
   Jean-Christophe Filliâtre (ENS Lyon, 1994-1997, LRI, 1997-2008)
+  Emilio Jesús Gallego Arias (MINES ParisTech 2015-now)
+  Gaetan Gilbert (INRIA-CoqHoTT 2016-now)
   Eduardo Giménez (ENS Lyon, 1993-1996, INRIA, 1997-1998)
   Stéphane Glondu (INRIA-PPS, 2007-2013)
   Benjamin Grégoire (INRIA, 2003-2011)
+  Jason Gross (MIT 2013-now)
   Hugo Herbelin (INRIA, 1996-now)
   Sébastien Hinderer (INRIA, 2014)
   Gérard Huet (INRIA, 1985-1997)
+  Matej Košík (INRIA, 2015-2017)
   Pierre Letouzey (LRI, 2000-2004, PPS, 2005-2008, INRIA-PPS, 2009-now)
   Patrick Loiseleur (Paris Sud, 1997-1999)
   Evgeny Makarov (INRIA, 2007)
+  Gregory Malecha (Harvard University 2013-2015,
+                   University of California, San Diego 2016)
+  Cyprien Mangin (INRIA-IRIF, 2015-now)
   Pascal Manoury (INRIA, 1993)
-  Micaela Mayero (INRIA, 1997-2002)
   Claude Marché (INRIA, 2003-2004 & LRI, 2004)
+  Micaela Mayero (INRIA, 1997-2002)
   Guillaume Melquiond (INRIA, 2009-now)
   Benjamin Monate (LRI, 2003)
   César Muñoz (INRIA, 1994-1995)
@@ -129,7 +141,8 @@ of the Coq Proof assistant during the indicated time:
   Catherine Parent-Vigouroux (ENS Lyon, 1992-1995)
   Christine Paulin-Mohring (INRIA, 1985-1989, ENS Lyon, 1989-1997,
                             LRI, 1997-2006)
-  Pierre-Marie Pédrot (INRIA-PPS, 2011-now)
+  Pierre-Marie Pédrot (INRIA-PPS, 2011-2015, INRIA-CoqHoTT 2015-2016,
+                       University of Ljubljana 2016-2017)
   Matthias Puech (INRIA-Bologna, 2008-2011)
   Yann Régis-Gianas (INRIA-PPS, 2009-now)
   Clément Renard (INRIA, 2001-2004)
@@ -138,9 +151,15 @@ of the Coq Proof assistant during the indicated time:
   Vincent Siles (INRIA, 2007)
   Élie Soubiran (INRIA, 2007-2010)
   Matthieu Sozeau (INRIA, 2005-now)
-  Arnaud Spiwack (INRIA, 2006-now)
+  Arnaud Spiwack (INRIA-LIX-Chalmers University, 2006-2010,
+                  INRIA, 2011-2014, MINES ParisTech 2014-2015,
+                  Tweag/IO 2015-now)
+  Paul Steckler (MIT 2016-now)
   Enrico Tassi (INRIA, 2011-now)
+  Amin Timany (Katholieke Universiteit Leuven, 2017)
   Benjamin Werner (INRIA, 1989-1994)
+  Nickolai Zeldovich (MIT 2014-2016)
+  Théo Zimmermann (INRIA-IRIF, 2015-now)
 
 ***************************************************************************
 INRIA refers to: