diff options
-rw-r--r-- | CONTRIBUTING.md | 2 | ||||
-rw-r--r-- | COPYRIGHT | 15 | ||||
-rw-r--r-- | CREDITS | 42 | ||||
-rw-r--r-- | dev/header | 10 |
4 files changed, 32 insertions, 37 deletions
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 74a138f14..213b87735 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -26,6 +26,8 @@ Documentation for getting started with the Coq sources is located in various fil Please make pull requests against the `master` branch. +If it's your first significant contribution to Coq (significant means: more than fixing a typo), your pull request should include a commit adding your name to the [`CREDITS`](/CREDITS) file (possibly with the name of your institution / employer if relevant to your contribution, an ORCID if you have one —you may log into https://orcid.org/ using your institutional account to get one—, and the year of your contribution). + It's helpful to run the Coq test suite with `make test-suite` before submitting your change. Travis CI runs this test suite and a much larger one including external Coq developments on every pull request, but these results take significantly longer to come back (on the order of a few hours). Running the test suite locally will take somewhere around 10-15 minutes. Refer to [`dev/ci/README.md`](/dev/ci/README.md#information-for-developers) for more information on Travis CI tests. If your pull request fixes a bug, please consider adding a regression test as well. See [`test-suite/README.md`](/test-suite/README.md) for how to do so. diff --git a/COPYRIGHT b/COPYRIGHT deleted file mode 100644 index fc4b7baa4..000000000 --- a/COPYRIGHT +++ /dev/null @@ -1,15 +0,0 @@ - The Coq proof assistant - -Copyright 1999-2016 The Coq development team, INRIA, CNRS, University -Paris Sud, University Paris 7, Ecole Polytechnique. - -This product includes also software developed by - Pierre Crégut, France Telecom R & D (plugins/omega and plugins/romega) - Pierre Courtieu and Julien Forest, CNAM (plugins/funind) - Claudio Sacerdoti Coen, HELM, University of Bologna, (plugins/xml) - Pierre Corbineau, Radboud University, Nijmegen (declarative mode) - John Harrison, University of Cambridge (csdp wrapper) - Georges Gonthier, Microsoft Research - Inria Joint Centre (plugins/ssrmatching) - -The file CREDITS contains a list of contributors. -The credits section in the Reference Manual details contributions. @@ -1,6 +1,6 @@ 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) @@ -8,7 +8,7 @@ The "Coq proof assistant" was jointly developed by - 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 Diderot - (Jan. 2009 - Dec. 2015). + (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). @@ -43,10 +43,15 @@ plugins/funind 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 @@ -57,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-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) theories/ZArith started by Pierre Crégut (France Telecom R&D, 1996) theories/Strings @@ -114,7 +117,7 @@ of the Coq Proof assistant during the indicated time: 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) + 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) @@ -123,12 +126,13 @@ of the Coq Proof assistant during the indicated time: 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) + 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-IRIF, 2015-now) + Cyprien Mangin (INRIA-PPS then IRIF, 2015-now) Pascal Manoury (INRIA, 1993) Claude Marché (INRIA, 2003-2004 & LRI, 2004) Micaela Mayero (INRIA, 1997-2002) @@ -141,10 +145,11 @@ 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-2015, INRIA-CoqHoTT 2015-2016, - University of Ljubljana 2016-2017) + Pierre-Marie Pédrot (INRIA-PPS, 2011-2015, INRIA-Ascola, 2015-2016, + University of Ljubljana, 2016-2017, + MPI-SWS, 2017-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) @@ -154,12 +159,13 @@ of the Coq Proof assistant during the indicated time: Arnaud Spiwack (INRIA-LIX-Chalmers University, 2006-2010, INRIA, 2011-2014, MINES ParisTech 2014-2015, Tweag/IO 2015-now) - Paul Steckler (MIT 2016-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 (INRIA-IRIF, 2015-now) + Théo Zimmermann (ORCID: https://orcid.org/0000-0002-3580-8806, + INRIA-PPS then IRIF, 2015-now) *************************************************************************** INRIA refers to: diff --git a/dev/header b/dev/header index bf7bdc169..7c3ee6004 100644 --- a/dev/header +++ b/dev/header @@ -1,7 +1,9 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) |