aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--doc/sphinx/refman-preamble.rst2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/refman-preamble.rst b/doc/sphinx/refman-preamble.rst
index a31d778af6..05e665a43b 100644
--- a/doc/sphinx/refman-preamble.rst
+++ b/doc/sphinx/refman-preamble.rst
@@ -14,7 +14,7 @@
.. |c_1| replace:: `c`\ :math:`_{1}`
.. |c_i| replace:: `c`\ :math:`_{i}`
.. |c_n| replace:: `c`\ :math:`_{n}`
-.. |Cic| replace:: :smallcaps:`Cic`
+.. |Cic| replace:: CIC
.. |Coq| replace:: :smallcaps:`Coq`
.. |CoqIDE| replace:: :smallcaps:`CoqIDE`
.. |eq_beta_delta_iota_zeta| replace:: `=`\ :math:`_{\beta\delta\iota\zeta}`