Imported Upstream version 8.8.2upstream/8.8.2

1 files changed, 47 insertions, 21 deletions

diff --git a/CREDITS b/CREDITS
index c6848648..7d9dfb49 100644
--- a/CREDITS
+++ b/CREDITS
@@ -1,13 +1,16 @@
 The "Coq proof assistant" was jointly developed by
-- INRIA Formel, Coq, LogiCal, ProVal, TypiCal, Marelle, pi.r2 projects
-  (starting 1985),
+- INRIA Formel, Coq, LogiCal, ProVal, TypiCal, Marelle,
+  pi.r2, Ascola, Galinette projects (starting 1985),
 - Laboratoire de l'Informatique du Parallelisme (LIP)
   associated to CNRS and ENS Lyon (Sep. 1989 to Aug. 1997),
 - Laboratoire de Recherche en Informatique (LRI)
   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 when it was merged into IRIF).
+- 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,13 +40,18 @@ 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)
+plugins/micromega
+  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)
 plugins/nsatz
   developed by Loïc Pottier (INRIA-Marelle, 2009-2011)
+plugins/omega
+  developed by Pierre Crégut (France Telecom R&D, 1996)
 plugins/quote
   developed by Patrick Loiseleur (LRI, 1997-1999)
 plugins/romega
@@ -54,16 +62,14 @@ plugins/setoid_ring
   developed by Benjamin Grégoire (INRIA-Everest, 2005-2006),
   Assia Mahboubi, Laurent Théry (INRIA-Marelle, 2006)
   and Bruno Barras (INRIA LogiCal, 2005-2006),
+plugins/ssreflect
+  developed by Georges Gonthier (Microsoft Research - Inria Joint Centre, 2007-2011),
+  Assia Mahboubi and Enrico Tassi (Inria, 2011-now).
 plugins/ssrmatching
   developed by Georges Gonthier (Microsoft Research - Inria Joint Centre, 2007-2011),
   and Enrico Tassi (Inria-Marelle, 2011-now)
 plugins/subtac
   developed by Matthieu Sozeau (LRI, 2005-2008)
-plugins/micromega
-  developed by Frédéric Besson (IRISA/INRIA, 2006-2008), 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)
 theories/ZArith
   started by Pierre Crégut (France Telecom R&D, 1996)
 theories/Strings
@@ -94,32 +100,42 @@ 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-Galinette, 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)
-  Pierre Letouzey (LRI, 2000-2004, PPS, 2005-2008, INRIA-PPS, 2009-now)
+  Matej Košík (INRIA, 2015-2017)
+  Pierre Letouzey (LRI, 2000-2004, PPS, 2005-2008,
+                   INRIA-PPS then IRIF, 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-PPS then 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,18 +145,28 @@ 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-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, 2009-now)
+  Yann Régis-Gianas (INRIA-PPS then IRIF, 2009-now)
   Clément Renard (INRIA, 2001-2004)
   Claudio Sacerdoti Coen (INRIA, 2004-2005)
   Amokrane Saïbi (INRIA, 1993-1998)
   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-2018)
   Enrico Tassi (INRIA, 2011-now)
+  Amin Timany (Katholieke Universiteit Leuven, 2017)
   Benjamin Werner (INRIA, 1989-1994)
+  Nickolai Zeldovich (MIT 2014-2016)
+  Théo Zimmermann (ORCID: https://orcid.org/0000-0002-3580-8806,
+                   INRIA-PPS then IRIF, 2015-now)
 
 ***************************************************************************
 INRIA refers to: