diff options
Diffstat (limited to 'doc/sphinx/replaces.rst')
| -rw-r--r-- | doc/sphinx/replaces.rst | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/doc/sphinx/replaces.rst b/doc/sphinx/replaces.rst index 1b2e17221..28a04f90c 100644 --- a/doc/sphinx/replaces.rst +++ b/doc/sphinx/replaces.rst @@ -35,7 +35,9 @@ .. |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` .. |mod_0| replace:: `mod`\ :math:`_{0}` .. |mod_1| replace:: `mod`\ :math:`_{1}` @@ -54,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}` |