diff options
Diffstat (limited to 'doc/sphinx/refman-preamble.rst')
| -rw-r--r-- | doc/sphinx/refman-preamble.rst | 62 |
1 files changed, 1 insertions, 61 deletions
diff --git a/doc/sphinx/refman-preamble.rst b/doc/sphinx/refman-preamble.rst index de95eda989..05e665a43b 100644 --- a/doc/sphinx/refman-preamble.rst +++ b/doc/sphinx/refman-preamble.rst @@ -11,60 +11,18 @@ .. role:: smallcaps -.. |A_1| replace:: `A`\ :math:`_{1}` -.. |A_n| replace:: `A`\ :math:`_{n}` -.. |arg_1| replace:: `arg`\ :math:`_{1}` -.. |arg_n| replace:: `arg`\ :math:`_{n}` -.. |bdi| replace:: :math:`\beta\delta\iota` -.. |binder_1| replace:: `binder`\ :math:`_{1}` -.. |binder_n| replace:: `binder`\ :math:`_{n}` -.. |binders_1| replace:: `binders`\ :math:`_{1}` -.. |binders_n| replace:: `binders`\ :math:`_{n}` -.. |C_1| replace:: `C`\ :math:`_{1}` .. |c_1| replace:: `c`\ :math:`_{1}` -.. |C_2| replace:: `C`\ :math:`_{2}` .. |c_i| replace:: `c`\ :math:`_{i}` .. |c_n| replace:: `c`\ :math:`_{n}` -.. |Cic| replace:: :smallcaps:`Cic` -.. |class_1| replace:: `class`\ :math:`_{1}` -.. |class_2| replace:: `class`\ :math:`_{2}` +.. |Cic| replace:: CIC .. |Coq| replace:: :smallcaps:`Coq` .. |CoqIDE| replace:: :smallcaps:`CoqIDE` .. |eq_beta_delta_iota_zeta| replace:: `=`\ :math:`_{\beta\delta\iota\zeta}` .. |Gallina| replace:: :smallcaps:`Gallina` -.. |ident_0| replace:: `ident`\ :math:`_{0}` -.. |ident_1,1| replace:: `ident`\ :math:`_{1,1}` -.. |ident_1,k_1| replace:: `ident`\ :math:`_{1,k_1}`) -.. |ident_1| replace:: `ident`\ :math:`_{1}` -.. |ident_2| replace:: `ident`\ :math:`_{2}` -.. |ident_3| replace:: `ident`\ :math:`_{3}` -.. |ident_i| replace:: `ident`\ :math:`_{i}` -.. |ident_j| replace:: `ident`\ :math:`_{j}` -.. |ident_k| replace:: `ident`\ :math:`_{k}` -.. |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}` -.. |mod_2| replace:: `mod`\ :math:`_{1}` -.. |mod_n| replace:: `mod`\ :math:`_{n}` -.. |module_0| replace:: `module`\ :math:`_{0}` -.. |module_1| replace:: `module`\ :math:`_{1}` -.. |module_expression_0| replace:: `module_expression`\ :math:`_{0}` -.. |module_expression_1| replace:: `module_expression`\ :math:`_{1}` -.. |module_expression_i| replace:: `module_expression`\ :math:`_{i}` -.. |module_expression_n| replace:: `module_expression`\ :math:`_{n}` -.. |module_n| replace:: `module`\ :math:`_{n}` -.. |module_type_0| replace:: `module_type`\ :math:`_{0}` -.. |module_type_1| replace:: `module_type`\ :math:`_{1}` -.. |module_type_i| replace:: `module_type`\ :math:`_{i}` -.. |module_type_n| replace:: `module_type`\ :math:`_{n}` -.. |N| replace:: ``N`` -.. |nat| replace:: ``nat`` .. |OCaml| replace:: :smallcaps:`OCaml` .. |p_1| replace:: `p`\ :math:`_{1}` .. |p_i| replace:: `p`\ :math:`_{i}` @@ -79,24 +37,6 @@ .. |t_i| replace:: `t`\ :math:`_{i}` .. |t_m| replace:: `t`\ :math:`_{m}` .. |t_n| replace:: `t`\ :math:`_{n}` -.. |f_1| replace:: `f`\ :math:`_{1}` -.. |f_i| replace:: `f`\ :math:`_{i}` -.. |f_m| replace:: `f`\ :math:`_{m}` -.. |f_n| replace:: `f`\ :math:`_{n}` -.. |u_1| replace:: `u`\ :math:`_{1}` -.. |u_i| replace:: `u`\ :math:`_{i}` -.. |u_m| replace:: `u`\ :math:`_{m}` -.. |u_n| replace:: `u`\ :math:`_{n}` -.. |term_0| replace:: `term`\ :math:`_{0}` -.. |term_1| replace:: `term`\ :math:`_{1}` -.. |term_2| replace:: `term`\ :math:`_{2}` -.. |term_n| replace:: `term`\ :math:`_{n}` -.. |type_0| replace:: `type`\ :math:`_{0}` -.. |type_1| replace:: `type`\ :math:`_{1}` -.. |type_2| replace:: `type`\ :math:`_{2}` -.. |type_3| replace:: `type`\ :math:`_{3}` -.. |type_n| replace:: `type`\ :math:`_{n}` .. |x_1| replace:: `x`\ :math:`_{1}` .. |x_i| replace:: `x`\ :math:`_{i}` .. |x_n| replace:: `x`\ :math:`_{n}` -.. |Z| replace:: ``Z`` |