From 7face8b53832621b733f900a4a92395c5ba97d34 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 2 Jan 2018 15:59:01 +0100 Subject: Remove redundant COPYRIGHT file. This information is already present in CREDITS. --- COPYRIGHT | 15 --------------- 1 file changed, 15 deletions(-) delete mode 100644 COPYRIGHT diff --git a/COPYRIGHT b/COPYRIGHT deleted file mode 100644 index fc4b7baa49..0000000000 --- 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. -- cgit v1.2.3 From f28813cfe8cac0193553aa1d009c76b3d26e743e Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 2 Jan 2018 16:00:29 +0100 Subject: Mention the CREDITS file in CONTRIBUTING. --- CONTRIBUTING.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 1a769333cc..450bae1be3 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. -- cgit v1.2.3 From 3457327ab61bff61df6c90d2b612d40fee99ccf7 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 2 Jan 2018 16:02:27 +0100 Subject: More accurate and complete headers. Remove the mention of specific labs (irrelevant for a copyright notice). Add a mention to represent other contributors and a pointer to CREDITS. --- dev/header | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/dev/header b/dev/header index bf7bdc1699..7c3ee60040 100644 --- a/dev/header +++ b/dev/header @@ -1,7 +1,9 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(*