diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 7 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 2 |
2 files changed, 2 insertions, 7 deletions
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index e5edd08995..3d1fc6d4b9 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -545,7 +545,7 @@ Computing Module dependencies In order to compute module dependencies (to be used by ``make`` or ``dune``), |Coq| provides the ``coqdep`` tool. -``coqdep`` computes inter-module dependencies for |Coq| and |OCaml| +``coqdep`` computes inter-module dependencies for |Coq| programs, and prints the dependencies on the standard output in a format readable by make. When a directory is given as argument, it is recursively looked at. @@ -554,11 +554,6 @@ Dependencies of |Coq| modules are computed by looking at ``Require`` commands (``Require``, ``Require Export``, ``Require Import``), but also at the command ``Declare ML Module``. -Dependencies of |OCaml| modules are computed by looking at -`open` commands and the dot notation *module.value*. However, this is -done approximately and you are advised to use ``ocamldep`` instead for the -|OCaml| module dependencies. - See the man page of ``coqdep`` for more details and options. Both Dune and ``coq_makefile`` use ``coqdep`` to compute the diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 36a5916868..2fa4f1fa42 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -275,7 +275,7 @@ These patterns can be used when the hypothesis is an equality: :n:`or` has multiple constructors (:n:`or_introl` and :n:`or_intror`), while :n:`and` has a single constructor (:n:`conj`) with multiple parameters (:n:`A` and :n:`B`). - These are defined in theories/Init/Logic.v. The "where" clauses define the + These are defined in ``theories/Init/Logic.v``. The "where" clauses define the infix notation for "or" and "and". .. coqdoc:: |