Convert vernac commands chapter to prodn, update syntax

2 files changed, 3 insertions, 1 deletions

diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index aa4b6edd7d..9d57864a07 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -379,7 +379,7 @@ Compiled libraries checker (coqchk)
 ----------------------------------------
 
 The ``coqchk`` command takes a list of library paths as argument, described either
-by their logical name or by their physical filename, hich must end in ``.vo``. The
+by their logical name or by their physical filename, which must end in ``.vo``. The
 corresponding compiled libraries (``.vo`` files) are searched in the path,
 recursively processing the libraries they depend on. The content of all these
 libraries is then type checked. The effect of ``coqchk`` is only to return with
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index d61e5ddce7..921c7bbbf7 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -42,6 +42,8 @@ As of today it is possible to build Coq projects using two tools:
 - coq_makefile, which is distributed by Coq and is based on generating a makefile,
 - Dune, the standard OCaml build tool, which, since version 1.9, supports building Coq libraries.
 
+.. _coq_makefile:
+
 Building a |Coq| project with coq_makefile
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~