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]

6 files changed, 58 insertions, 39 deletions

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 7b2229cb7..2dffd2019 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -22,21 +22,30 @@ If you want to minimize your bug (or help minimize someone else's) for more extr
 
 If you want to contribute a bug fix or feature yourself, pull requests on the [GitHub repository](https://github.com/coq/coq) are the way to contribute directly to the Coq implementation. We recommend you create a fork of the repository on GitHub and push your changes to a new "topic branch" in that fork. From there you can follow the [GitHub pull request documentation](https://help.github.com/articles/about-pull-requests/) to get your changes reviewed and pulled into the Coq source repository.
 
-Documentation for getting started with the Coq sources is located in various files in [`dev/doc`](/dev/doc) (for example, [debugging.md](/dev/doc/debugging.md)). For further help with the Coq sources, feel free to join the [Coq Gitter chat](https://gitter.im/coq/coq) and ask questions.
+Documentation for getting started with the Coq sources is located in various
+files in [`dev/doc`](dev/doc) (for example, [debugging.md](dev/doc/debugging.md)).
+For further help with the Coq sources, feel free to join
+the [Coq Gitter chat](https://gitter.im/coq/coq) and ask questions.
 
 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).
+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. Our CI runs this test suite and lots of other tests, including
 building 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
+[`dev/ci/README.md`](dev/ci/README.md#information-for-developers) for more
 information on CI tests, including how to run them on your private branches.
 
-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.
+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.
 
 Don't be alarmed if the pull request process takes some time. It can take a few days to get feedback, approval on the final changes, and then a merge. Coq doesn't release new versions very frequently so it can take a few months for your change to land in a released version. That said, you can start using the latest Coq `master` branch to take advantage of all the new features, improvements, and fixes.
 
@@ -48,7 +57,8 @@ Here are a few tags Coq developers may add to your PR and what they mean. In gen
 - [needs: fixing](https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+fixing%22) indicates the PR needs a fix, as discussed in the comments.
 - [needs: benchmarking](https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+benchmarking%22) and [needs: testing](https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+testing%22) indicate the PR needs testing beyond what the test suite can handle. For example, performance benchmarking is currently performed with a different infrastructure. Unless some followup is specifically requested you aren't expected to do this additional testing.
 
-To learn more about the merging process, you can read the [merging documentation for Coq maintainers](/dev/doc/MERGING.md).
+To learn more about the merging process, you can read the
+[merging documentation for Coq maintainers](dev/doc/MERGING.md).
 
 ## Documentation
 
diff --git a/README.md b/README.md
index 4956da36d..0903abdd4 100644
--- a/README.md
+++ b/README.md
@@ -14,11 +14,11 @@ environment for semi-interactive development of machine-checked proofs.
 ## Installation
 Download the pre-built packages of the [latest release](https://github.com/coq/coq/releases/latest) for Windows and MacOS;
 read the [help page](https://coq.inria.fr/opam/www/using.html) on how to install Coq with OPAM;
-or refer to the [`INSTALL` file](/INSTALL) for the procedure to install from source.
+or refer to the [`INSTALL` file](INSTALL) for the procedure to install from source.
 
 ## Documentation
 
-The sources of the documentation can be found in directory [`doc`](/doc). The
+The sources of the documentation can be found in directory [`doc`](doc). The
 documentation of the last released version is available on the Coq
 web site at [coq.inria.fr/documentation](http://coq.inria.fr/documentation).
 See also [Cocorico](https://github.com/coq/coq/wiki) (the Coq wiki),
@@ -26,7 +26,7 @@ and the [Coq FAQ](https://github.com/coq/coq/wiki/The-Coq-FAQ),
 for additional user-contributed documentation.
 
 ## Changes
-There is a file named [`CHANGES`](/CHANGES) that explains the differences and the
+There is a file named [`CHANGES`](CHANGES) that explains the differences and the
 incompatibilities since last versions. If you upgrade Coq, please read
 it carefully.
 
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
diff --git a/test-suite/README.md b/test-suite/README.md
index ef2e574ec..e81da0830 100644
--- a/test-suite/README.md
+++ b/test-suite/README.md
@@ -62,20 +62,26 @@ BUILDING SUMMARY FILE
 NO FAILURES
 ```
 
-See [`test-suite/Makefile`](/test-suite/Makefile) for more information.
+See [`test-suite/Makefile`](Makefile) for more information.
 
 ## Adding a test
 
-Regression tests for closed bugs should be added to `test-suite/bugs/closed`, as `1234.v` where `1234` is the bug number.
+Regression tests for closed bugs should be added to
+[`bugs/closed`](bugs/closed), as `1234.v` where `1234` is the bug number.
 Files in this directory are tested for successful compilation.
 When you fix a bug, you should usually add a regression test here as well.
 
-The error "(bug seems to be opened, please check)" when running `make test-suite` means that a test in `bugs/closed` failed to compile.
+The error "(bug seems to be opened, please check)" when running
+`make test-suite` means that a test in [`bugs/closed`](bugs/closed) failed to
+compile.
 
-There are also output tests in `test-suite/output` which consist of a `.v` file and a `.out` file with the expected output.
+There are also output tests in [`output`](output) which consist of a `.v` file
+and a `.out` file with the expected output.
 
-There are unit tests of OCaml code in `test-suite/unit-tests`. These tests are contained in `.ml` files, and rely on the `OUnit`
-unit-test framework, as described at http://ounit.forge.ocamlcore.org/.  Use `make unit-tests' in the unit-tests directory to run them.
+There are unit tests of OCaml code in [`unit-tests`](unit-tests). These tests
+are contained in `.ml` files, and rely on the `OUnit` unit-test framework, as
+described at <http://ounit.forge.ocamlcore.org/>.  Use `make unit-tests` in the
+[`unit-tests`](unit-tests) directory to run them.
 
 ## Fixing output tests
 
@@ -88,5 +94,5 @@ automatically.
 Don't forget to check the updated `.out` files into git!
 
 Note that `output/MExtraction.out` is special: it is copied from
-`micromega/micromega.ml` in the plugin source directory. Automatic
-approval will incorrectly update the copy.
+[`micromega/micromega.ml`](../plugins/micromega/micromega.ml) in the plugin
+source directory. Automatic approval will incorrectly update the copy.