diff options
Diffstat (limited to 'doc/sphinx/refman-preamble.rst')
| -rw-r--r-- | doc/sphinx/refman-preamble.rst | 98 |
1 files changed, 98 insertions, 0 deletions
diff --git a/doc/sphinx/refman-preamble.rst b/doc/sphinx/refman-preamble.rst new file mode 100644 index 0000000000..aa581e1ee1 --- /dev/null +++ b/doc/sphinx/refman-preamble.rst @@ -0,0 +1,98 @@ +.. This file is automatically prepended to all other files using the ``rst_prolog`` option. + +.. only:: html + + .. This is included once per page in the HTML build, and a single time (in the + document's preamble) in the LaTeX one. + + .. preamble:: /refman-preamble.sty + +.. Some handy replacements for common items + +.. 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}` +.. |Coq| replace:: :smallcaps:`Coq` +.. |CoqIDE| replace:: :smallcaps:`CoqIDE` +.. |eq_beta_delta_iota_zeta| replace:: `=`\ :math:`_{\small{\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}` +.. |p_n| replace:: `p`\ :math:`_{n}` +.. |Program| replace:: :strong:`Program` +.. |SSR| replace:: :smallcaps:`SSReflect` +.. |t_1| replace:: `t`\ :math:`_{1}` +.. |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`` |