From 4c9ba141f8f7e067f274cb5a02293e8e52f89487 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Fri, 27 Mar 2020 21:23:27 -0700
Subject: Convert vernac commands chapter to prodn, update syntax

---
 doc/sphinx/practical-tools/coq-commands.rst | 2 +-
 doc/sphinx/practical-tools/utilities.rst    | 2 ++
 2 files changed, 3 insertions(+), 1 deletion(-)

(limited to 'doc/sphinx/practical-tools')

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
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-- 
cgit v1.2.3