aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/sphinx/replaces.rst
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-04-13 11:05:48 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-04-14 15:44:29 +0200
commit3cc6a433d025996ea4a61969517d45ffbc9fd8a9 (patch)
tree6846570d84758373da6bffa36b3bb8e285703aa4 /doc/sphinx/replaces.rst
parent14f44c0e23c413314adf23ed1059acc5cd1fef2f (diff)
[sphinx] Fix many warnings.
Including cross-reference TODOs. I took down the number of warnings from 300 to 50.
Diffstat (limited to 'doc/sphinx/replaces.rst')
-rw-r--r--doc/sphinx/replaces.rst3
1 files changed, 2 insertions, 1 deletions
diff --git a/doc/sphinx/replaces.rst b/doc/sphinx/replaces.rst
index 0fee3754b..28a04f90c 100644
--- a/doc/sphinx/replaces.rst
+++ b/doc/sphinx/replaces.rst
@@ -35,6 +35,7 @@
.. |ident_n,1| replace:: `ident`\ :math:`_{n,1}`
.. |ident_n,k_n| replace:: `ident`\ :math:`_{n,k_n}`
.. |ident_n| replace:: `ident`\ :math:`_{n}`
+.. |Latex| replace:: :smallcaps:`LaTeX`
.. |L_tac| replace:: `L`:sub:`tac`
.. |Ltac| replace:: `L`:sub:`tac`
.. |ML| replace:: :smallcaps:`ML`
@@ -55,7 +56,7 @@
.. |module_type_n| replace:: `module_type`\ :math:`_{n}`
.. |N| replace:: ``N``
.. |nat| replace:: ``nat``
-.. |Ocaml| replace:: :smallcaps:`OCaml`
+.. |OCaml| replace:: :smallcaps:`OCaml`
.. |p_1| replace:: `p`\ :math:`_{1}`
.. |p_i| replace:: `p`\ :math:`_{i}`
.. |p_n| replace:: `p`\ :math:`_{n}`