Markdown docs: switch from absolute to relative links.

We had mostly used absolute links in the past.
I just discovered that GitHub recommends using relative links instead:
https://help.github.com/articles/basic-writing-and-formatting-syntax/#relative-links
and indeed my Emacs Markdown mode can handle relative links but doesn't
interpret absolute links relatively to the root of the git repository.

[ci skip]

3 files changed, 26 insertions, 23 deletions

diff --git a/dev/ci/README.md b/dev/ci/README.md
index dc586c61f..665b3768a 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -47,15 +47,15 @@ CI.
 
 ### Add your development by submitting a pull request
 
-Add a new `ci-mydev.sh` script to [`dev/ci`](/dev/ci) (have a look at
-[`ci-coq-dpdgraph.sh`](/dev/ci/ci-coq-dpdgraph.sh) or
-[`ci-fiat-parsers.sh`](/dev/ci/ci-fiat-parsers.sh) for simple examples);
+Add a new `ci-mydev.sh` script to [`dev/ci`](.) (have a look at
+[`ci-coq-dpdgraph.sh`](ci-coq-dpdgraph.sh) or
+[`ci-fiat-parsers.sh`](ci-fiat-parsers.sh) for simple examples);
 set the corresponding variables in
-[`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh); add the corresponding
-target to [`Makefile.ci`](/Makefile.ci); add new jobs to
-[`.gitlab-ci.yml`](/.gitlab-ci.yml),
-[`.circleci/config.yml`](/.circleci/config.yml) and
-[`.travis.yml`](/.travis.yml) so that this new target is run. **Do not
+[`ci-basic-overlay.sh`](ci-basic-overlay.sh); add the corresponding
+target to [`Makefile.ci`](../../Makefile.ci); add new jobs to
+[`.gitlab-ci.yml`](../../.gitlab-ci.yml),
+[`.circleci/config.yml`](../../.circleci/config.yml) and
+[`.travis.yml`](../../.travis.yml) so that this new target is run. **Do not
 hesitate to submit an incomplete pull request if you need help to finish it.**
 
 You may also be interested in having your development tested in our
@@ -83,7 +83,7 @@ We are currently running tests on the following platforms:
 
 - Travis CI is used to test the compilation of Coq and run the test-suite on
   macOS. It also runs a linter that checks whitespace discipline. A
-  [pre-commit hook](/dev/tools/pre-commit) is automatically installed by
+  [pre-commit hook](../tools/pre-commit) is automatically installed by
   `./configure`. It should allow complying with this discipline without pain.
 
 - AppVeyor is used to test the compilation of Coq and run the test-suite on
@@ -92,7 +92,7 @@ We are currently running tests on the following platforms:
 GitLab CI and Travis CI and AppVeyor support putting `[ci skip]` in a commit
 message to bypass CI. Do not use this unless your commit only changes files
 that are not compiled (e.g. Markdown files like this one, or files under
-[`.github/`](/.github/)).
+[`.github/`](../../.github/)).
 
 You can anticipate the results of most of these tests prior to submitting your
 PR by running GitLab CI on your private branches. To do so follow these steps:
@@ -112,7 +112,7 @@ there are some.
 
 You can also run one CI target locally (using `make ci-somedev`).
 
-See also [`test-suite/README.md`](/test-suite/README.md) for information about adding new tests to the test-suite.
+See also [`test-suite/README.md`](../../test-suite/README.md) for information about adding new tests to the test-suite.
 
 ### Breaking changes
 
@@ -123,7 +123,7 @@ patch (or ask someone to prepare a patch) to fix the project:
    the project to your changes.
 2. Test your pull request with your adapted version of the external project by
    adding an overlay file to your pull request (cf.
-   [`dev/ci/user-overlays/README.md`](/dev/ci/user-overlays/README.md)).
+   [`dev/ci/user-overlays/README.md`](user-overlays/README.md)).
 3. Fixes to external libraries (pure Coq projects) *must* be backward
    compatible (i.e. they should also work with the development version of Coq,
    and the latest stable version). This will allow you to open a PR on the
@@ -137,7 +137,7 @@ patch (or ask someone to prepare a patch) to fix the project:
    developer who merges the PR on Coq. There are plans to improve this, cf.
    [#6724](https://github.com/coq/coq/issues/6724).
 
-Moreover your PR must absolutely update the [`CHANGES`](/CHANGES) file.
+Moreover your PR must absolutely update the [`CHANGES`](../../CHANGES) file.
 
 Advanced GitLab CI information
 ------------------------------
@@ -173,8 +173,9 @@ automatically built and uploaded to your GitLab registry, and is
 loaded by subsequent jobs.
 
 **IMPORTANT**: When updating Coq's CI docker image, you must modify
-the `CACHEKEY` variable in `.gitlab-ci.yml`, `.circleci/config.yml`,
-and `Dockerfile`.
+the `CACHEKEY` variable in [`.gitlab-ci.yml`](../../.gitlab-ci.yml),
+[`.circleci/config.yml`](../../.circleci/config.yml),
+and [`Dockerfile`](docker/bionic_coq/Dockerfile)
 
 The Docker building job reuses the uploaded image if it is available,
 but if you wish to save more time you can skip the job by setting
@@ -182,4 +183,6 @@ but if you wish to save more time you can skip the job by setting
 
 This means you will need to change its value when the Docker image
 needs to be updated. You can do so for a single pipeline by starting
-it through the web interface.
+it through the web interface..
+
+See also [`docker/README.md`](docker/README.md).
diff --git a/dev/ci/user-overlays/README.md b/dev/ci/user-overlays/README.md
index aec2dfe0a..41212568d 100644
--- a/dev/ci/user-overlays/README.md
+++ b/dev/ci/user-overlays/README.md
@@ -6,7 +6,7 @@ request to test it with the adapted version of the external project.
 
 An overlay is a file which defines where to look for the patched version so that
 testing is possible. It redefines some variables from
-[`ci-basic-overlay.sh`](/dev/ci/ci-basic-overlay.sh):
+[`ci-basic-overlay.sh`](../ci-basic-overlay.sh):
 give the name of your branch using a `_CI_BRANCH` variable and the location of
 your fork using a `_CI_GITURL` variable.
 
@@ -28,4 +28,4 @@ if [ "$CI_PULL_REQUEST" = "669" ] || [ "$CI_BRANCH" = "ssr-merge" ]; then
 fi
 ```
 
-(`CI_PULL_REQUEST` and `CI_BRANCH` are set in [`ci-common.sh`](/dev/ci/ci-common.sh))
+(`CI_PULL_REQUEST` and `CI_BRANCH` are set in [`ci-common.sh`](../ci-common.sh))
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
index 65457b63a..0b4078a7c 100644
--- a/dev/doc/MERGING.md
+++ b/dev/doc/MERGING.md
@@ -6,7 +6,7 @@ This document describes how patches, submitted as pull requests (PRs) on the
 
 ## Code owners
 
-The [CODEOWNERS](/.github/CODEOWNERS) file describes, for each part of the
+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.
 
@@ -51,10 +51,10 @@ say in a comment they think a review is not required and proceed with the merge.
 
 If the PR breaks compatibility of some external projects in CI, then fixes to
 those external projects should have been prepared (cf. the relevant sub-section
-in the [CI README](/dev/ci/README.md#Breaking-changes) and the PR can be tested
-with these fixes thanks to ["overlays"](/dev/ci/user-overlays/README.md).
+in the [CI README](../ci/README.md#Breaking-changes) and the PR can be tested
+with these fixes thanks to ["overlays"](../ci/user-overlays/README.md).
 
-Moreover the PR must absolutely update the [`CHANGES`](/CHANGES) file.
+Moreover the PR must absolutely update the [`CHANGES`](../../CHANGES) file.
 
 If overlays are missing, ask the author to prepare them and label the PR with
 the [needs: overlay](https://github.com/coq/coq/labels/needs%3A%20overlay) label.
@@ -74,7 +74,7 @@ Once all reviewers approved the PR, the assignee is expected to check that CI
 completed without relevant failures, and that the PR comes with appropriate
 documentation and test cases. If not, they should leave a comment on the PR and
 put the approriate label. Otherwise, they are expected to merge the PR using the
-[merge script](/dev/tools/merge-pr.sh).
+[merge script](../tools/merge-pr.sh).
 
 When the PR has conflicts, the assignee can either:
 - ask the author to rebase the branch, fixing the conflicts