Refine a bit the decentralized merging process.

We make GitHub assign only principal maintainers as reviewers. This
reduces the level of noise (PRs with 10 code owners), and makes it easy
for the assignee to check if all reviews have been completed (all
reviewers in the list have to approve the PR, which was not the case
before if two reviewers were assigned for the same component).

This change means that when a principal maintainer submits a patch
touching the component they own, they should ask a review from the
secondary maintainer.

2 files changed, 266 insertions, 91 deletions

diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index b64212dff..9a33abad6 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -1,124 +1,295 @@
 # This file describes the maintainers for the main components. See
 # `dev/doc/MERGING.md`.
 
-# component-path  principal-maintainer secondary-maintainer
+########## GitHub metadata, including this file ##########
 
-# GitHub metadata, including this file
-/.github/         @maximedenes @Zimmi48
+/.github/         @maximedenes
+# Secondary maintainer @Zimmi48
 
-# CI infrastructure
-/dev/ci/*.sh      @ejgallego @SkySkimmer
-/.travis.yml      @ejgallego @SkySkimmer
-/.gitlab-ci.yml   @SkySkimmer @ejgallego
-/.appveyor.yml    @maximedenes @SkySkimmer
+########## CI infrastructure ##########
 
-/default.nix     @Zimmi48 @vbgl
+/dev/ci/*.sh      @ejgallego
+# Secondary maintainer @SkySkimmer
 
-# Documentation
-/README.md        @Zimmi48 @maximedenes
-/INSTALL*         @Zimmi48 @maximedenes
-/CONTRIBUTING.md  @Zimmi48 @maximedenes
-/dev/doc/         @Zimmi48 @maximedenes
-/doc/             @silene @maximedenes
-/man/             @silene @maximedenes
+/.travis.yml      @ejgallego
+# Secondary maintainer @SkySkimmer
 
-/checker/         @barras @maximedenes
+/.gitlab-ci.yml   @SkySkimmer
+# Secondary maintainer @ejgallego
 
-/clib/            @ppedrot @ejgallego
+/.appveyor.yml    @maximedenes
+# Secondary maintainer @SkySkimmer
 
+/default.nix     @Zimmi48
+# Secondary maintainer @vbgl
 
-/engine/          @ppedrot @aspiwack
+########## Documentation ##########
 
-/grammar/         @ppedrot @maximedenes
+/README.md        @Zimmi48
+# Secondary maintainer @maximedenes
 
-/ide/             @ppedrot @gares
+/INSTALL*         @Zimmi48
+# Secondary maintainer @maximedenes
 
-/interp/          @herbelin @ejgallego
+/CONTRIBUTING.md  @Zimmi48
+# Secondary maintainer @maximedenes
 
-/intf/            @letouzey @ppedrot
-/kernel/          @maximedenes @barras
-/kernel/byterun/  @maximedenes @silene
-/lib/             @ejgallego @ppedrot
-/library/         @silene @gares
+/dev/doc/         @Zimmi48
+# Secondary maintainer @maximedenes
 
-/parsing/         @herbelin @mattam82
+/doc/             @silene
+# Secondary maintainer @maximedenes
 
-/plugins/btauto/  @ppedrot @herbelin
+/man/             @silene
+# Secondary maintainer @maximedenes
+
+########## Coqchk ##########
+
+/checker/         @barras
+# Secondary maintainer @maximedenes
+
+########## Coq lib ##########
+
+/clib/            @ppedrot
+# Secondary maintainer @ejgallego
+
+/lib/             @ejgallego
+# Secondary maintainer @ppedrot
+
+########## Proof engine ##########
+
+/engine/          @ppedrot
+# Secondary maintainer @aspiwack
+
+########## Grammar macros ##########
+
+/grammar/         @ppedrot
+# Secondary maintainer @maximedenes
+
+########## CoqIDE ##########
+
+/ide/             @ppedrot
+# Secondary maintainer @gares
+
+########## Interpretation ##########
+
+/interp/          @herbelin
+# Secondary maintainer @ejgallego
+
+########## Interfaces ##########
+
+/intf/            @letouzey
+# Secondary maintainer @ppedrot
+
+########## Kernel ##########
+
+/kernel/          @maximedenes
+# Secondary maintainer @barras
+
+/kernel/byterun/  @maximedenes
+# Secondary maintainer @silene
+
+########## Library ##########
+
+/library/         @silene
+# Secondary maintainer @gares
+
+########## Parser ##########
+
+/parsing/         @herbelin
+# Secondary maintainer @mattam82
+
+########## Plugins ##########
+
+/plugins/btauto/  @ppedrot
+# Secondary maintainer @herbelin
 
 # I don't know Pierre Corbineau's GitHub nickname
 /plugins/cc/            @herbelin
 
-/plugins/derive/        @aspiwack @ppedrot
-/plugins/extraction/    @letouzey @maximedenes
+/plugins/derive/        @aspiwack
+# Secondary maintainer @ppedrot
 
- # I don't know Pierre Corbineau's GitHub nickname
+/plugins/extraction/    @letouzey
+# Secondary maintainer @maximedenes
+
+# I don't know Pierre Corbineau's GitHub nickname
 /plugins/firstorder/    @herbelin
 
-/plugins/fourier/       @herbelin @gares
-/plugins/funind/        @forestjulien @Matafou
+/plugins/fourier/       @herbelin
+# Secondary maintainer @gares
+
+/plugins/funind/        @forestjulien
+# Secondary maintainer @Matafou
+
 /plugins/ltac/          @ppedrot
-/plugins/micromega/     @fajb @bgregoir
-/plugins/nsatz/         @thery @ppedrot
+# Secondary maintainer @herbelin
+
+/plugins/micromega/     @fajb
+# Secondary maintainer @bgregoir
+
+/plugins/nsatz/         @thery
+# Secondary maintainer @ppedrot
+
 /plugins/omega/         @letouzey
+
 /plugins/romega/        @letouzey
-/plugins/setoid_ring/   @amahboubi @bgregoir
-/plugins/ssrmatching/   @gares @maximedenes
-/plugins/ssr/           @gares @maximedenes
-/plugins/syntax/        @ppedrot @maximedenes
 
+/plugins/setoid_ring/   @amahboubi
+# Secondary maintainer @bgregoir
+
+/plugins/ssrmatching/   @gares
+# Secondary maintainer @maximedenes
+
+/plugins/ssr/           @gares
+# Secondary maintainer @maximedenes
+
+/plugins/syntax/        @ppedrot
+# Secondary maintainer @maximedenes
 
 /plugins/quote/ @herbelin
 
 # Should be Pierre Corbineau too
 /plugins/rtauto/ @herbelin
 
-/pretyping/       @mattam82 @gares
-/printing/        @herbelin @mattam82
-
-/proofs/          @ppedrot @Zimmi48
-
-/stm/             @gares @ejgallego
-
-/tactics/         @ppedrot @mattam82
-
-/theories/Arith/          @letouzey @herbelin
-/theories/Bool/           @letouzey @herbelin
-/theories/Classes/        @mattam82 @herbelin
-/theories/FSets/          @letouzey @herbelin
-/theories/Init/           @letouzey @ppedrot
-/theories/Lists/          @letouzey @ppedrot
-/theories/Logic/          @herbelin @ppedrot
-/theories/MSets/          @letouzey @herbelin
-/theories/NArith/         @letouzey @herbelin
-/theories/Numbers/        @letouzey @herbelin
-/theories/PArith/         @letouzey @herbelin
-/theories/Program/        @mattam82 @herbelin
-/theories/QArith/         @letouzey @herbelin
-/theories/Reals/          @silene @ppedrot
-/theories/Relations/      @mattam82 @ppedrot
-/theories/Setoids/        @mattam82 @ppedrot
-/theories/Sets/           @letouzey @herbelin
-/theories/Sorting/        @letouzey @herbelin
-/theories/Strings/        @letouzey @herbelin
-/theories/Structures/     @letouzey @herbelin
-/theories/Unicode/        @letouzey @herbelin
-/theories/Wellfounded/    @letouzey @mattam82
-/theories/ZArith/         @letouzey @herbelin
-
-/theories/Compat/         @JasonGross @Zimmi48
+########## Pretyper ##########
+
+/pretyping/       @mattam82
+# Secondary maintainer @gares
+
+########## Pretty printer ##########
+
+/printing/        @herbelin
+# Secondary maintainer @mattam82
+
+########## Proof infrastructure ##########
+
+/proofs/          @ppedrot
+# Secondary maintainer @Zimmi48
+
+########## STM ##########
+
+/stm/             @gares
+# Secondary maintainer @ejgallego
+
+########## Tactics ##########
+
+/tactics/         @ppedrot
+# Secondary maintainer @mattam82
+
+########## Standard library ##########
+
+/theories/Arith/          @letouzey
+# Secondary maintainer @herbelin
+
+/theories/Bool/           @letouzey
+# Secondary maintainer @herbelin
+
+/theories/Classes/        @mattam82
+# Secondary maintainer @herbelin
+
+/theories/FSets/          @letouzey
+# Secondary maintainer @herbelin
+
+/theories/Init/           @letouzey
+# Secondary maintainer @ppedrot
+
+/theories/Lists/          @letouzey
+# Secondary maintainer @ppedrot
+
+/theories/Logic/          @herbelin
+# Secondary maintainer @ppedrot
+
+/theories/MSets/          @letouzey
+# Secondary maintainer @herbelin
+
+/theories/NArith/         @letouzey
+# Secondary maintainer @herbelin
+
+/theories/Numbers/        @letouzey
+# Secondary maintainer @herbelin
+
+/theories/PArith/         @letouzey
+# Secondary maintainer @herbelin
+
+/theories/Program/        @mattam82
+# Secondary maintainer @herbelin
+
+/theories/QArith/         @letouzey
+# Secondary maintainer @herbelin
+
+/theories/Reals/          @silene
+# Secondary maintainer @ppedrot
+
+/theories/Relations/      @mattam82
+# Secondary maintainer @ppedrot
+
+/theories/Setoids/        @mattam82
+# Secondary maintainer @ppedrot
+
+/theories/Sets/           @letouzey
+# Secondary maintainer @herbelin
+
+/theories/Sorting/        @letouzey
+# Secondary maintainer @herbelin
+
+/theories/Strings/        @letouzey
+# Secondary maintainer @herbelin
+
+/theories/Structures/     @letouzey
+# Secondary maintainer @herbelin
+
+/theories/Unicode/        @letouzey
+# Secondary maintainer @herbelin
+
+/theories/Wellfounded/    @letouzey
+# Secondary maintainer @mattam82
+
+/theories/ZArith/         @letouzey
+# Secondary maintainer @herbelin
+
+/theories/Compat/         @JasonGross
+# Secondary maintainer @Zimmi48
 
 /theories/Vectors/        @herbelin
 
-/tools/coqdoc/          @silene @mattam82
-/tools/coq_makefile*    @gares @silene
-/tools/CoqMakefile*     @gares @silene
-/tools/coqdep*          @ppedrot @maximedenes
-/tools/coq_tex*         @silene @gares
-/tools/coqwc*           @silene @gares
+########## Tools ##########
+
+/tools/coqdoc/          @silene
+# Secondary maintainer @mattam82
+
+/tools/coq_makefile*    @gares
+# Secondary maintainer @silene
+
+/tools/CoqMakefile*     @gares
+# Secondary maintainer @silene
+
+/tools/coqdep*          @ppedrot
+# Secondary maintainer @maximedenes
+
+/tools/coq_tex*         @silene
+# Secondary maintainer @gares
+
+/tools/coqwc*           @silene
+# Secondary maintainer @gares
+
+########## Toplevel ##########
+
+/toplevel/        @ejgallego
+# Secondary maintainer @gares
+
+########## Vernacular ##########
+
+/vernac/          @mattam82
+# Secondary maintainer @maximedenes
+
+########## Build system ##########
+
+/Makefile*        @letouzey
+# Secondary maintainer @maximdenes
 
-/toplevel/        @ejgallego @gares
-/vernac/          @mattam82 @maximedenes
+/configure*       @letouzey
+# Secondary maintainer @ejgallego
 
-/Makefile*        @letouzey @ejgallego
-/configure*       @letouzey @ejgallego
-/META.coq         @letouzey @ejgallego
+/META.coq         @letouzey
+# Secondary maintainer @ejgallego
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
index df366a978..f1dddbd0e 100644
--- a/dev/doc/MERGING.md
+++ b/dev/doc/MERGING.md
@@ -9,19 +9,23 @@ The [CODEOWNERS](/.github/CODEOWNERS) file describes, for each part of the
 system, two owners. One is the principal maintainer of the component, the other
 is the secondary maintainer.
 
-When a pull request is submitted, GitHub will automatically ask these two
-maintainers for a review. If the pull request touches several parts, all the
-corresponding maintainers will be asked for a review.
+When a pull request is submitted, GitHub will automatically ask the principal
+maintainer for a review. If the pull request touches several parts, all the
+corresponding principal maintainers will be asked for a review.
 
 Maintainers are never assigned as reviewer on their own PRs.
 
+If a principal maintainer submits a PR that changes the component they own, they
+must assign the secondary maintainer as reviewer. They should also do it if they
+know they are not available to do the review.
+
 ## Reviewing
 
-When principal maintainers receive a review request, they are expected to:
+When maintainers receive a review request, they are expected to:
 
 * Put their name in the assignee field, if they are in charge of the component
-  that is the main target of the patch (or if they are the only principal
-  maintainer asked to review the PR).
+  that is the main target of the patch (or if they are the only maintainer asked
+  to review the PR).
 * Review the PR, approve it or request changes.
 * If they are the assignee, check if all reviewers approved the PR. If not,
   regularly ping the author (if changes should be implemented) or the reviewers