diff options
Diffstat (limited to 'doc/sphinx/refman-preamble.rst')
| -rw-r--r-- | doc/sphinx/refman-preamble.rst | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/doc/sphinx/refman-preamble.rst b/doc/sphinx/refman-preamble.rst index 05e665a43b..e67405a8dc 100644 --- a/doc/sphinx/refman-preamble.rst +++ b/doc/sphinx/refman-preamble.rst @@ -20,7 +20,6 @@ .. |eq_beta_delta_iota_zeta| replace:: `=`\ :math:`_{\beta\delta\iota\zeta}` .. |Gallina| replace:: :smallcaps:`Gallina` .. |Latex| replace:: :smallcaps:`LaTeX` -.. |L_tac| replace:: `L`:sub:`tac` .. |Ltac| replace:: `L`:sub:`tac` .. |ML| replace:: :smallcaps:`ML` .. |OCaml| replace:: :smallcaps:`OCaml` |