[doc] [INSTALL] Port INSTALL to markdown format.

6 files changed, 330 insertions, 327 deletions

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index e26103cedd..99e394efa3 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -865,7 +865,7 @@ team.
 #### Building Coq ####
 
 The list of dependencies can be found in the first section of the
-[`INSTALL`](INSTALL) file.
+[`INSTALL.md`](INSTALL.md) file.
 
 Today, the recommended method for building Coq is to use `dune`.  Run
 `make -f Makefile.dune` to get help on the various available targets,
diff --git a/INSTALL b/INSTALL
deleted file mode 100644
index 31758203fe..0000000000
--- a/INSTALL
+++ /dev/null
@@ -1,323 +0,0 @@
-            INSTALLING FROM SOURCES
-            -----------------------
-
-
-WHAT DO YOU NEED ?
-==================
-
-   To compile Coq yourself, you need:
-
-   - OCaml (version >= 4.05.0)
-     (available at https://ocaml.org/)
-     (This version of Coq has been tested up to OCaml 4.09.0)
-
-   - The Num package, which used to be part of the OCaml standard library,
-     if you are using an OCaml version >= 4.06.0
-
-   - Findlib (version >= 1.4.1)
-     (available at http://projects.camlcity.org/projects/findlib.html)
-
-   - GNU Make version 3.81 or later
-
-   - a C compiler
-
-   - an IEEE-754 compliant architecture with rounding to nearest
-     ties to even as default rounding mode (most architectures
-     should work nowadays)
-
-   - for CoqIDE, the lablgtk development files (version >= 3.0.0),
-     and the GTK 3.x libraries including gtksourceview3.
-
-   The IEEE-754 compliance is required by primitive floating-point
-   numbers (Require Import Floats). Common sources of incompatibility
-   are checked at configure time, preventing compilation. In the,
-   unlikely, event an incompatibility remains undetected, using Floats
-   would enable to prove False on this architecture.
-
-   Note that num and lablgtk should be properly registered with
-   findlib/ocamlfind as Coq's makefile will use it to locate the
-   libraries during the build.
-
-   Debian / Ubuntu users can get the necessary system packages for
-   CoqIDE with:
-
-   $ sudo apt-get install libgtksourceview-3.0-dev
-
-   Opam (https://opam.ocaml.org/) is recommended to install OCaml and
-   the corresponding packages.
-
-   $ opam install num ocamlfind lablgtk3-sourceview3
-
-   should get you a reasonable OCaml environment to compile Coq.
-
-   Nix users can also get all the required dependencies by running:
-
-   $ nix-shell
-
-   Advanced users may want to experiment with the OCaml Flambda
-   compiler as way to improve the performance of Coq. In order to
-   profit from Flambda, a special build of the OCaml compiler that has
-   the Flambda optimizer enabled must be installed. For OPAM users,
-   this amounts to installing a compiler switch ending in `+flambda`,
-   such as `4.07.0+flambda`. For other users, YMMV. Once `ocamlopt
-   -config` reports that Flambda is available, some further
-   optimization options can be used; see the entry about -flambda-opts
-   below for more details.
-
-QUICK INSTALLATION PROCEDURE.
-=============================
-
-1. ./configure
-2. make
-3. make install (you may need superuser rights)
-
-INSTALLATION PROCEDURE IN DETAILS (NORMAL USERS).
-=================================================
-
-1- Check that you have the OCaml compiler installed on your
-   computer and that "ocamlc" (or, better, its native code version
-   "ocamlc.opt") lies in a directory which is present in your $PATH
-   environment variable. At the time of writing this sentence, all
-   versions of Objective Caml later or equal to 4.05.0 are
-   supported.
-
-   To get Coq in native-code, (it runs 4 to 10 times faster than
-   bytecode, but it takes more time to get compiled and the binary is
-   bigger), you will also need the "ocamlopt" (or its native code version
-   "ocamlopt.opt") command.
-
-2- The uncompression and un-tarring of the distribution file gave birth
-   to a directory named "coq-8.xx". You can rename this directory and put
-   it wherever you want. Just keep in mind that you will need some spare
-   space during the compilation (reckon on about 300 Mb of disk space
-   for the whole system in native-code compilation). Once installed, the
-   binaries take about 30 Mb, and the library about 200 Mb.
-
-3- First you need to configure the system. It is done automatically with
-   the command:
-
-	./configure <options>
-
-   The "configure" script will ask you for directories where to put
-   the Coq binaries, standard library, man pages, etc. It will propose
-   you some default values.
-
-   For a list of options accepted by the "configure" script, run
-   "./configure -help". The main options accepted are:
-
--prefix <dir>
-	Binaries, library, and man pages will be respectively
-	installed in <dir>/bin, <dir>/lib/coq, and <dir>/man
-
--bindir <dir>                   (default: /usr/local/bin)
-        Directory where the binaries will be installed
-
--libdir <dir>                   (default: /usr/local/lib/coq)
-        Directory where the Coq standard library will be installed
-
--mandir <dir>                   (default: /usr/local/share/man)
-        Directory where the Coq manual pages will be installed
-
--arch <value>			(default is the result of the command "arch")
-	An arbitrary architecture name for your machine (useful when
-	compiling Coq on two different architectures for which the
-	result of "arch" is the same, e.g. Sun OS and Solaris)
-
--local
-        Compile Coq to run in its source directory. The installation (step 6)
-        is not necessary in that case.
-
--browser <command>
-	Use <command> to open an URL in a browser. %s must appear in <command>,
-	and will be replaced by the URL.
-
--flambda-opts <flags>
-        This experimental option will pass specific user flags to the
-        OCaml optimizing compiler. In most cases, this option is used
-        to tweak the flambda backend; for maximum performance we
-        recommend using
-
-        -flambda-opts `-O3 -unbox-closures`
-
-        but of course you are free to try with a different combination
-        of flags. You can read more at
-        https://caml.inria.fr/pub/docs/manual-ocaml/flambda.html
-
-        There is a known problem with certain OCaml versions and
-        `native_compute`, that will make compilation to require
-        a large amount of RAM (>= 10GiB) in some particular files.
-
-        We recommend disabling native compilation (`-native-compiler no`)
-        with flambda unless you use OCaml >= 4.07.0.
-
-        c.f. https://caml.inria.fr/mantis/view.php?id=7630
-
-   If you want your build to be reproducible, ensure that the
-   SOURCE_DATE_EPOCH environment variable is set as documented in
-   https://reproducible-builds.org/specs/source-date-epoch/
-
-4- Still in the root directory, do
-
-	make
-
-   to compile Coq in the best OCaml mode available (native-code if supported,
-   bytecode otherwise).
-
-   This will compile the entire system. This phase can take more or less time,
-   depending on your architecture and is fairly verbose. On a multi-core machine,
-   it is recommended to compile in parallel, via make -jN where N is your number
-   of cores.
-
-5- You can now install the Coq system. Executables, libraries, and
-   manual pages are copied in some standard places of your system,
-   defined at configuration time (step 3). Just do
-
-	umask 022
-       	make install
-
-   Of course, you may need superuser rights to do that.
-
-6- Optionally, you could build the bytecode version of Coq via:
-
-        make byte
-
-   and install it via
-
-        make install-byte
-
-  This version is quite slower than the native code version of Coq, but could
-  be helpful for debugging purposes. In particular, coqtop.byte embeds an OCaml
-  toplevel accessible via the Drop command.
-
-7- You can now clean all the sources. (You can even erase them.)
-
-	make clean
-
-
-INSTALLATION PROCEDURE FOR ADVANCED USERS.
-==========================================
-
-   If you wish to write plugins you *must* keep the Coq sources, without
-   cleaning them. Therefore, to avoid a duplication of binaries and library,
-   it is not necessary to do the installation step (6- above).  You just have
-   to tell it at configuration step (4- above) with the option -local :
-
-	./configure -local <other options>
-
-   Then compile the sources as described in step 5 above. The resulting
-   binaries will reside in the subdirectory bin/.
-
-   Unless you pass the -nodebug option to ./configure, the -g option of the
-   OCaml compiler will be used during compilation to allow debugging.
-   See the debugging file in dev/doc and the chapter 15 of the Coq Reference
-   Manual for details about how to use the OCaml debugger with Coq.
-
-
-THE AVAILABLE COMMANDS.
-=======================
-
-   There are two Coq commands:
-
-	coqtop		The Coq toplevel
-	coqc		The Coq compiler
-
-   Under architecture where ocamlopt is available, coqtop is the native code
-   version of Coq. On such architecture, you could additionally request
-   the build of the bytecode version of Coq via 'make byte' and install it via
-   'make install-byte'. This will create  an extra binary named coqtop.byte,
-   that could be used for debugging purpose. If native code isn't available,
-   coqtop.byte is directly built by 'make', and coqtop is a link to coqtop.byte.
-   coqc also invokes the fastest version of Coq. Options -opt and -byte to coqtop
-   and coqc selects a particular binary.
-
-    * `coqtop' launches Coq in the interactive mode. By default it loads
-      basic logical definitions and tactics from the Init directory.
-
-    * `coqc' allows compilation of Coq files directly from the command line.
-      To compile a file foo.v, do:
-
-		coqc foo.v
-
-      It will produce a file foo.vo, that you can now load through the Coq
-      command "Require".
-
-   A detailed description of these commands and of their options is given
-   in the Reference Manual (which you can get in the doc/
-   directory, or read online on http://coq.inria.fr/doc/)
-   and in the corresponding manual pages.
-
-
-COMPILING FOR DIFFERENT ARCHITECTURES.
-======================================
-
-   This section explains how to compile Coq for several architecture, sharing
-   the same sources. The important fact is that some files are architecture
-   dependent (.cmx, .o and executable files for instance) but others are not
-   (.cmo and .vo). Consequently, you can :
-
-   o  save some time during compilation by not cleaning the architecture
-      independent files;
-
-   o  save some space during installation by sharing the Coq standard
-      library (which is fully architecture independent).
-
-   So, in order to compile Coq for a new architecture, proceed as follows:
-
-   * Omit step 7 above and clean only the architecture dependent files:
-     it is done automatically with the command
-
-		make archclean
-
-   * Configure the system for the new architecture:
-
-		./configure <options>
-
-     You can specify the same directory for the standard library but you
-     MUST specify a different directory for the binaries (of course).
-
-   * Compile and install the system as described in steps 5 and 6 above.
-
-
-MOVING BINARIES OR LIBRARY.
-===========================
-
-   If you move both the binaries and the library in a consistent way,
-   Coq should be able to still run. Otherwise, Coq may be "lost",
-   running "coqtop" would then return an error message of the kind:
-
-	Error during initialization :
-	Error: cannot guess a path for Coq libraries; please use -coqlib option
-
-   You can then indicate the new places to Coq, using the options -coqlib :
-
-	coqtop -coqlib <new directory>
-
-   See also next section.
-
-
-DYNAMICALLY LOADED LIBRARIES FOR BYTECODE EXECUTABLES.
-======================================================
-
-   Some bytecode executables of Coq use the OCaml runtime, which dynamically
-   loads a shared library (.so or .dll). When it is not installed properly, you
-   can get an error message of this kind:
-
-	Fatal error: cannot load shared library dllcoqrun
-	Reason: dllcoqrun.so: cannot open shared object file: No such file or directory
-
-   In this case, you need either:
-     - to set the CAML_LD_LIBRARY_PATH environment variable to point to the
-       directory where dllcoqrun.so is; this is suitable when you want to run
-       the command a limited number of times in a controlled environment (e.g.
-       during compilation of binary packages);
-     - install dllcoqrun.so in a location listed in the file ld.conf that is in
-       the directory of the standard library of OCaml;
-     - recompile your bytecode executables after reconfiguring the location
-       of the shared library:
-         ./configure -vmbyteflags "-dllib,-lcoqrun,-dllpath,<path>" ...
-       where <path> is the directory where the dllcoqrun.so is installed;
-     - (not recommended) compile bytecode executables with a custom OCaml
-       runtime by using:
-         ./configure -custom ...
-       be aware that stripping executables generated this way, or performing
-       other executable-specific operations, will make them useless.
diff --git a/INSTALL.md b/INSTALL.md
new file mode 100644
index 0000000000..03ec26c3b3
--- /dev/null
+++ b/INSTALL.md
@@ -0,0 +1,326 @@
+Installing From Sources
+=======================
+
+What Do You Need ?
+------------------
+
+To compile Coq yourself, you need:
+
+- [OCaml](https://ocaml.org/) (version >= 4.05.0)
+  (This version of Coq has been tested up to OCaml 4.09.0)
+
+- The [num](https://github.com/ocaml/num) library; note that it is
+  included in the OCaml distribution for OCaml versions < 4.06.0
+
+- The [findlib](http://projects.camlcity.org/projects/findlib.html) library (version >= 1.8.0)
+
+- GNU Make (version >= 3.81)
+
+- a C compiler
+
+- an IEEE-754 compliant architecture with rounding to nearest
+  ties to even as default rounding mode (most architectures
+  should work nowadays)
+
+- for CoqIDE, the
+  [lablgtk3-sourceview3](https://github.com/garrigue/lablgtk) library
+  (version >= 3.0.beta8), and the corresponding GTK 3.x libraries, as
+  of today (gtk+3 >= 3.18 and gtksourceview3 >= 3.18)
+
+The IEEE-754 compliance is required by primitive floating-point
+numbers (`Require Import Floats`). Common sources of incompatibility
+are checked at configure time, preventing compilation. In the,
+unlikely, event an incompatibility remains undetected, using Floats
+would enable to prove False on this architecture.
+
+Note that `num` and `lablgtk3-sourceview3` should be properly
+registered with `findlib/ocamlfind` as Coq's makefile will use it to
+locate the libraries during the build.
+
+Debian / Ubuntu users can get the necessary system packages for
+CoqIDE with:
+
+    $ sudo apt-get install libgtksourceview-3.0-dev
+
+Opam (https://opam.ocaml.org/) is recommended to install OCaml and
+the corresponding packages.
+
+    $ opam switch create coq 4.09.0+flambda
+    $ eval $(opam env)
+    $ opam install num ocamlfind lablgtk3-sourceview3
+
+should get you a reasonable OCaml environment to compile Coq. See the
+OPAM documentation for more help.
+
+Nix users can also get all the required dependencies by running:
+
+    $ nix-shell
+
+Advanced users may want to experiment with the OCaml Flambda
+compiler as way to improve the performance of Coq. In order to
+profit from Flambda, a special build of the OCaml compiler that has
+the Flambda optimizer enabled must be installed. For OPAM users,
+this amounts to installing a compiler switch ending in `+flambda`,
+such as `4.07.1+flambda`. For other users, YMMV. Once `ocamlopt
+-config` reports that Flambda is available, some further
+optimization options can be used; see the entry about -flambda-opts
+below for more details.
+
+Quick Installation Procedure.
+-----------------------------
+
+    $ ./configure
+    $ make
+    $ make install (you may need superuser rights)
+
+Installation Procedure In Details (Normal Users).
+-------------------------------------------------
+
+1. Check that you have the OCaml compiler installed on your
+   computer and that `ocamlc` (or, better, its native code version
+   `ocamlc.opt`) lies in a directory which is present in your $PATH
+   environment variable. At the time of writing this sentence, all
+   versions of Objective Caml later or equal to 4.05.0 are
+   supported.
+
+   To get Coq in native-code, (it runs 4 to 10 times faster than
+   bytecode, but it takes more time to get compiled and the binary is
+   bigger), you will also need the `ocamlopt` (or its native code version
+   `ocamlopt.opt`) command.
+
+2. The uncompression and un-tarring of the distribution file gave birth
+   to a directory named "coq-8.xx". You can rename this directory and put
+   it wherever you want. Just keep in mind that you will need some spare
+   space during the compilation (reckon on about 300 Mb of disk space
+   for the whole system in native-code compilation). Once installed, the
+   binaries take about 30 Mb, and the library about 200 Mb.
+
+3. First you need to configure the system. It is done automatically with
+   the command:
+
+        ./configure <options>
+
+   The `configure` script will ask you for directories where to put
+   the Coq binaries, standard library, man pages, etc. It will propose
+   you some default values.
+
+   For a list of options accepted by the `configure` script, run
+   `./configure -help`. The main options accepted are:
+
+   * `-prefix <dir>`
+     Binaries, library, and man pages will be respectively
+     installed in `<dir>/bin`, `<dir>/lib/coq`, and `<dir>/man`
+
+   * `-bindir <dir>`                   (default: `/usr/local/bin`)
+     Directory where the binaries will be installed
+
+   * `-libdir <dir>`                   (default: `/usr/local/lib/coq`)
+     Directory where the Coq standard library will be installed
+
+   * `-mandir <dir>`                   (default: `/usr/local/share/man`)
+     Directory where the Coq manual pages will be installed
+
+   * `-arch <value>`                   (default is the result of the command `arch`)
+     An arbitrary architecture name for your machine (useful when
+     compiling Coq on two different architectures for which the
+     result of "arch" is the same, e.g. Sun OS and Solaris)
+
+   * `-local`
+     Compile Coq to run in its source directory. The installation (step 6)
+     is not necessary in that case.
+
+   * `-browser <command>`
+     Use <command> to open an URL in a browser. %s must appear in <command>,
+     and will be replaced by the URL.
+
+   * `-flambda-opts <flags>`
+     This experimental option will pass specific user flags to the
+     OCaml optimizing compiler. In most cases, this option is used
+     to tweak the flambda backend; for maximum performance we
+     recommend using:
+
+         -flambda-opts `-O3 -unbox-closures`
+
+     but of course you are free to try with a different combination
+     of flags. You can read more at
+     https://caml.inria.fr/pub/docs/manual-ocaml/flambda.html
+
+     There is a known problem with certain OCaml versions and
+     `native_compute`, that will make compilation to require
+     a large amount of RAM (>= 10GiB) in some particular files.
+
+     We recommend disabling native compilation (`-native-compiler no`)
+     with flambda unless you use OCaml >= 4.07.0.
+
+     c.f. https://caml.inria.fr/mantis/view.php?id=7630
+
+   If you want your build to be reproducible, ensure that the
+   SOURCE_DATE_EPOCH environment variable is set as documented in
+   https://reproducible-builds.org/specs/source-date-epoch/
+
+4. Still in the root directory, do
+
+        make
+
+   to compile Coq in the best OCaml mode available (native-code if supported,
+   bytecode otherwise).
+
+   This will compile the entire system. This phase can take more or less time,
+   depending on your architecture and is fairly verbose. On a multi-core machine,
+   it is recommended to compile in parallel, via make -jN where N is your number
+   of cores.
+
+5. You can now install the Coq system. Executables, libraries, and
+   manual pages are copied in some standard places of your system,
+   defined at configuration time (step 3). Just do
+
+        umask 022
+        make install
+
+   Of course, you may need superuser rights to do that.
+
+6. Optionally, you could build the bytecode version of Coq via:
+
+        make byte
+
+   and install it via
+
+        make install-byte
+
+  This version is quite slower than the native code version of Coq, but could
+  be helpful for debugging purposes. In particular, coqtop.byte embeds an OCaml
+  toplevel accessible via the Drop command.
+
+7. You can now clean all the sources. (You can even erase them.)
+
+        make clean
+
+Installation Procedure For Advanced Users.
+------------------------------------------
+
+If you wish to write plugins you *must* keep the Coq sources, without
+cleaning them. Therefore, to avoid a duplication of binaries and library,
+it is not necessary to do the installation step (6- above).  You just have
+to tell it at configuration step (4- above) with the option -local :
+
+    ./configure -local <other options>
+
+Then compile the sources as described in step 5 above. The resulting
+binaries will reside in the subdirectory bin/.
+
+Unless you pass the -nodebug option to ./configure, the -g option of the
+OCaml compiler will be used during compilation to allow debugging.
+See the debugging file in dev/doc and the chapter 15 of the Coq Reference
+Manual for details about how to use the OCaml debugger with Coq.
+
+
+The Available Commands.
+-----------------------
+
+There are two Coq commands:
+
+    coqtop          The Coq toplevel
+    coqc            The Coq compiler
+
+Under architecture where ocamlopt is available, coqtop is the native code
+version of Coq. On such architecture, you could additionally request
+the build of the bytecode version of Coq via 'make byte' and install it via
+'make install-byte'. This will create  an extra binary named coqtop.byte,
+that could be used for debugging purpose. If native code isn't available,
+coqtop.byte is directly built by 'make', and coqtop is a link to coqtop.byte.
+coqc also invokes the fastest version of Coq. Options -opt and -byte to coqtop
+and coqc selects a particular binary.
+
+* `coqtop` launches Coq in the interactive mode. By default it loads
+  basic logical definitions and tactics from the Init directory.
+
+* `coqc` allows compilation of Coq files directly from the command line.
+  To compile a file foo.v, do:
+
+        coqc foo.v
+
+  It will produce a file `foo.vo`, that you can now load through the Coq
+  command `Require`.
+
+  A detailed description of these commands and of their options is given
+  in the Reference Manual (which you can get in the doc/
+  directory, or read online on http://coq.inria.fr/doc/)
+  and in the corresponding manual pages.
+
+Compiling For Different Architectures.
+--------------------------------------
+
+This section explains how to compile Coq for several architecture, sharing
+the same sources. The important fact is that some files are architecture
+dependent (`.cmx`, `.o` and executable files for instance) but others are not
+(`.cmo` and `.vo`). Consequently, you can :
+
+-  save some time during compilation by not cleaning the architecture
+   independent files;
+
+-  save some space during installation by sharing the Coq standard
+   library (which is fully architecture independent).
+
+So, in order to compile Coq for a new architecture, proceed as follows:
+
+* Omit step 7 above and clean only the architecture dependent files:
+  it is done automatically with the command
+
+        make archclean
+
+* Configure the system for the new architecture:
+
+        ./configure <options>
+
+  You can specify the same directory for the standard library but you
+  MUST specify a different directory for the binaries (of course).
+
+* Compile and install the system as described in steps 5 and 6 above.
+
+Moving Binaries Or Library.
+---------------------------
+
+If you move both the binaries and the library in a consistent way,
+Coq should be able to still run. Otherwise, Coq may be "lost",
+running "coqtop" would then return an error message of the kind:
+
+    Error during initialization :
+    Error: cannot guess a path for Coq libraries; please use -coqlib option
+
+You can then indicate the new places to Coq, using the options -coqlib :
+
+    coqtop -coqlib <new directory>
+
+See also next section.
+
+Dynamically Loaded Libraries For Bytecode Executables.
+------------------------------------------------------
+
+Some bytecode executables of Coq use the OCaml runtime, which dynamically
+loads a shared library (.so or .dll). When it is not installed properly, you
+can get an error message of this kind:
+
+    Fatal error: cannot load shared library dllcoqrun
+    Reason: dllcoqrun.so: cannot open shared object file: No such file or directory
+
+In this case, you need either:
+
+- to set the `CAML_LD_LIBRARY_PATH` environment variable to point to the
+  directory where dllcoqrun.so is; this is suitable when you want to run
+  the command a limited number of times in a controlled environment (e.g.
+  during compilation of binary packages);
+- install dllcoqrun.so in a location listed in the file ld.conf that is in
+  the directory of the standard library of OCaml;
+- recompile your bytecode executables after reconfiguring the location
+  of the shared library:
+
+        ./configure -vmbyteflags "-dllib,-lcoqrun,-dllpath,<path>" ...
+
+  where `<path>` is the directory where the dllcoqrun.so is installed;
+- (not recommended) compile bytecode executables with a custom OCaml
+  runtime by using:
+
+        ./configure -custom ...
+
+  be aware that stripping executables generated this way, or performing
+  other executable-specific operations, will make them useless.
diff --git a/README.md b/README.md
index d3d5057be9..ffbeb22327 100644
--- a/README.md
+++ b/README.md
@@ -54,7 +54,7 @@ environment for semi-interactive development of machine-checked proofs.
 
 Download the pre-built packages of the [latest release][] for Windows and macOS;
 read the [help page][opam-using] on how to install Coq with OPAM;
-or refer to the [`INSTALL`](INSTALL) file for the procedure to install from source.
+or refer to the [`INSTALL.md`](INSTALL.md) file for the procedure to install from source.
 
 [latest release]: https://github.com/coq/coq/releases/latest
 [opam-using]: https://coq.inria.fr/opam/www/using.html
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 82cc7a7117..b1c752ba60 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -1385,7 +1385,7 @@ function copy_coq_license {
     # FIXME: this is not the micromega license
     # It only applies to code that was copied into one single file!
     install -D README.md                      "$PREFIXCOQ/license_readme/coq/ReadMe.md"
-    install -D INSTALL                        "$PREFIXCOQ/license_readme/coq/Install.txt"
+    install -D INSTALL.md                     "$PREFIXCOQ/license_readme/coq/Install.txt"
     install -D doc/README.md                  "$PREFIXCOQ/license_readme/coq/ReadMeDoc.md" || true
   fi
 }
diff --git a/doc/README.md b/doc/README.md
index b784fe92f6..ef3ccc2105 100644
--- a/doc/README.md
+++ b/doc/README.md
@@ -27,7 +27,7 @@ Dependencies
 ### HTML documentation
 
 To produce the complete documentation in HTML, you will need Coq dependencies
-listed in [`INSTALL`](../INSTALL). Additionally, the Sphinx-based
+listed in [`INSTALL.md`](../INSTALL.md). Additionally, the Sphinx-based
 reference manual requires Python 3, and the following Python packages:
 
   - sphinx >= 1.7.8