Tentatively updating credits while remaining brief.

2 files changed, 34 insertions, 43 deletions

diff --git a/CREDITS b/CREDITS
index b05917930..9a6db78a0 100644
--- a/CREDITS
+++ b/CREDITS
@@ -1,5 +1,4 @@
 The "Coq proof assistant" was jointly developed by
-
 - INRIA Formel, Coq, LogiCal, ProVal, TypiCal, Marelle, pi.r2 projects
   (starting 1985),
 - Laboratoire de l'Informatique du Parallelisme (LIP)
@@ -27,16 +26,12 @@ the GNU Lesser General Public License Version 2.1.
 
 plugins/cc
   developed by Pierre Corbineau (ENS Cachan, 2001, LRI, 2001-2005, Radboud
-  University at Nijmegen, 2005-2008)
-plugins/correctness
-  developed by Jean-Christophe Filliâtre (LRI, 1999-2001)
-plugins/dp
-  developed by Nicolas Ayache (LRI, 2005-2006) and Jean-Christophe Filliâtre
-  (LRI, 2005-2008)
+  University at Nijmegen, 2005-2008, Grenoble 1, 2010-2014)
+plugins/decl_mode
+  developed by Pierre Corbineau (Radboud University at Nijmegen, 2005-2008,
+  Grenoble 1, 2009-2011)
 plugins/extraction
   developed by Pierre Letouzey (LRI, 2000-2004, PPS, 2005-now)
-plugins/field
-  developed by David Delahaye and Micaela Mayero (INRIA-LogiCal, 2001)
 plugins/firstorder
   developed by Pierre Corbineau (LRI, 2003-2008)
 plugins/fourier
@@ -48,10 +43,9 @@ plugins/funind
 plugins/omega
   developed by Pierre Crégut (France Telecom R&D, 1996)
 plugins/nsatz
-  developed by Loïc Pottier (INRIA-Marelle, 2009)
-plugins/ring
-  developed by Samuel Boutin (INRIA-Coq, 1996) and Patrick
-  Loiseleur (LRI, 1997-1999)
+  developed by Loïc Pottier (INRIA-Marelle, 2009-2011)
+plugins/quote
+  developed by Patrick Loiseleur (LRI, 1997-1999)
 plugins/romega
   developed by Pierre Crégut (France Telecom R&D, 2001-2004)
 plugins/rtauto
@@ -62,51 +56,43 @@ plugins/setoid_ring
   and Bruno Barras (INRIA LogiCal, 2005-2006),
 plugins/subtac
   developed by Matthieu Sozeau (LRI, 2005-2008)
-plugins/xml
-  developed by Claudio Sacerdoti (Univ. Bologna, 2000-2005)
-  as part of the HELM and MoWGLI projects; extension by Cezary Kaliszyk as
-  part of the ProofWeb project (Radboud University at Nijmegen, 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)
-parsing/search.ml
-  mainly developed by Yves Bertot (INRIA-Lemme, 2000-2004)
 theories/ZArith
   started by Pierre Crégut (France Telecom R&D, 1996)
 theories/Strings
   developed by Laurent Théry (INRIA-Lemme, 2003)
 theories/Numbers/Cyclic
-  developed by Benjamin Grégoire (INRIA-Everest, 2007), Laurent Théry (INRIA-Marelle, 2007-2008), Arnaud Spiwack (INRIA-LogiCal, 2007) and Pierre Letouzey (PPS, 2008)
+  developed by Benjamin Grégoire (INRIA-Everest, 2007),
+  Laurent Théry (INRIA-Marelle, 2007-2008),
+  Arnaud Spiwack (INRIA-LogiCal, 2007) and Pierre Letouzey (PPS, 2008)
 ide/utils
   some files come from Maxence Guesdon's Cameleon tool
 
-Many discussions within the INRIA teams and labs taking part to the
-development influenced the design of Coq especially with
-
-  C. Auger, Y. Bertot, F. Blanqui, J. Courant, P. Courtieu, J. Duprat,
-  S. Glondu, J. Goubault, J.-P. Jouannaud, S. Lescuyer, A. Mahboubi,
-  C. Marché, A. Miquel, B. Monate, L. Pottier, Y. Régis-Gianas,
-  P.-Y. Strub, L. Théry, B. Werner
+The development of Coq significantly benefited from feedback,
+suggestions or short contributions from the following non exhaustive
+list of persons and groups:
 
-The development of Coq also significantly benefited from feedback,
-suggestions or short contributions from:
-
-  C. Alvarado, P. Crégut, J.-F. Monin (France Telecom R&D),
-  P. Castéran (University Bordeaux 1),
+  C. Alvarado, C. Auger, F. Blanqui, P. Castéran, C. Cohen,
+  J. Courant, J. Duprat, F. Garillot, G. Gonthier, J. Goubault,
+  J.-P. Jouannaud, S. Lescuyer, A. Miquel, J.-F. Monin, P.-Y. Strub
   the Foundations Group (Radboud University, Nijmegen, The Netherlands),
   Laboratoire J.-A. Dieudonné (University of Nice-Sophia Antipolis),
-  F. Garillot, G. Gonthier (INRIA-MSR joint lab),
   INRIA-Gallium project,
   the CS dept at Yale, the CIS dept at U. Penn,
-  the CSE dept at Harvard, the CS dept at Princeton
+  the CSE dept at Harvard, the CS dept at Princeton, the CS dept at MIT
+  as well as a lot of users on coq-club, coqdev, coq-bugs
 
 The following people have contributed to the development of different versions
 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)
+  Xavier Clerc (INRIA, 2012-2014)
   Jacek Chrzaszcz (LRI, 1998-2003)
   Thierry Coquand (INRIA, 1985-1989)
   Pierre Corbineau (LRI, 2003-2005, Nijmegen, 2005-2008, Grenoble 1, 2008-2011)
@@ -115,14 +101,16 @@ of the Coq Proof assistant during the indicated time:
   David Delahaye (INRIA, 1997-2002)
   Maxime Dénès (INRIA, 2013-now)
   Daniel de Rauglaudre (INRIA, 1996-1998)
+  Maxime Dénès (INRIA, 2013-now)
   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)
   Eduardo Giménez (ENS Lyon, 1993-1996, INRIA, 1997-1998)
-  Stéphane Glondu (INRIA-PPS, 2007-now)
+  Stéphane Glondu (INRIA-PPS, 2007-2013)
   Benjamin Grégoire (INRIA, 2003-2011)
   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)
   Patrick Loiseleur (Paris Sud, 1997-1999)
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index 8c169ee1e..ef7a61931 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -959,7 +959,7 @@ The way Coq processes a document in batch and interactive mode has
 been redesigned by Enrico Tassi with help from Bruno Barras.  Opaque
 proofs, the text between Proof and Qed, can be processed
 asynchronously, decoupling the checking of definitions and statements
-from the checking of proofs.  In interactively this improves the
+from the checking of proofs.  In interactive use, this improves the
 reactiveness of the system, since proofs can be processed in the
 background.  Similarly the compilation of a file can be split into two
 phases:  the first one checking only definitions and statements and
@@ -967,15 +967,18 @@ the second one checking proofs.  A file resulting from the first
 phase, .vio extension, can be already Required.  All .vio files can be
 turned into complete .vo files in parallel.  The same infrastructure
 also allows terminating tactics to be run in parallel on a set of
-goals via the par: goal selector.
-CoqIDE was patched to cope with asynchronous checking of the document.
+goals via the \verb=par:= goal selector.
+
+CoqIDE was modified to cope with asynchronous checking of the document.
 Its source code was also made separate from the one of Coq making it no
 more a special user interface and allowing its release cycle to be
 decoupled with the one of Coq.
-Carst Tankink developed a Coq back end for PIDE enabled user interfaces,
-like PIDE/jEdit (with help from Makarius Wenzel) or PIDE/Coqoon (with
-help from Alexander Faithfull and Jesper Bengtson).
-The development of such features was funded by the Paral-ITP ANR project.
+
+Carst Tankink developed a Coq back end for user interfaces built on
+Makarius Wenzel's Prover IDE framework (PIDE), like PIDE/jEdit (with
+help from Makarius Wenzel) or PIDE/Coqoon (with help from Alexander
+Faithfull and Jesper Bengtson).  The development of such features was
+funded by the Paral-ITP French ANR project.
 
 The universe polymorphism extension is based on a change of the kernel
 architecture to handle constraint checking only, leaving the generation
@@ -999,7 +1002,7 @@ the relations between homotopy theory and type theory.
 {\Coq} 8.5 also comes with a bunch of many various smaller-scale changes
 and improvements regarding the different components of the system.
 
-High-Level Specification Language: 
+High-Level Specification Language:
 - tactics in terms
 - Universe inconsistency and unification error messages
 - Named existentials