diff options
Diffstat (limited to 'doc/sphinx/practical-tools/coq-commands.rst')
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 958d295219..545bba4930 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -380,7 +380,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 |