diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-04-14 21:57:53 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-04-14 21:59:15 +0200 |
| commit | ab2e6772c6cbe2e6fa8851a1b399222a2a7740e3 (patch) | |
| tree | 8bd8a4bd811af8a57f7b675741221a5a9c849511 /doc/sphinx/language/coq-library.rst | |
| parent | 3cc6a433d025996ea4a61969517d45ffbc9fd8a9 (diff) | |
[Sphinx] Fix all remaining warnings.
Diffstat (limited to 'doc/sphinx/language/coq-library.rst')
| -rw-r--r-- | doc/sphinx/language/coq-library.rst | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index c5da866b8..6af6e7897 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -48,6 +48,7 @@ at the |Coq| root directory; this includes the modules ``Tactics``. Module ``Logic_Type`` also makes it in the initial state. +.. _init-notations: Notations ~~~~~~~~~ @@ -929,9 +930,8 @@ tactics (see Chapter :ref:`tactics`), there are also: Goal forall x y z:R, x * y * z <> 0. intros; split_Rmult. -These tactics has been written with the tactic language Ltac -described in Chapter :ref:`thetacticlanguage`. - +These tactics has been written with the tactic language |Ltac| +described in Chapter :ref:`ltac`. List library ~~~~~~~~~~~~ |