From b3dadd37aa1a9ca8c6be377edb46832b4f3b7256 Mon Sep 17 00:00:00 2001 From: Clément Pit-Claudel Date: Thu, 17 May 2018 20:56:04 -0400 Subject: [doc] Include the rst and LaTeX preambles automatically in all files --- doc/sphinx/README.rst | 2 +- doc/sphinx/README.template.rst | 2 +- doc/sphinx/addendum/canonical-structures.rst | 1 - doc/sphinx/addendum/extended-pattern-matching.rst | 2 - doc/sphinx/addendum/extraction.rst | 2 - doc/sphinx/addendum/generalized-rewriting.rst | 3 - doc/sphinx/addendum/implicit-coercions.rst | 2 - doc/sphinx/addendum/miscellaneous-extensions.rst | 2 - doc/sphinx/addendum/nsatz.rst | 2 - doc/sphinx/addendum/parallel-proof-processing.rst | 2 - doc/sphinx/addendum/program.rst | 3 - doc/sphinx/addendum/ring.rst | 2 - doc/sphinx/addendum/type-classes.rst | 2 - doc/sphinx/addendum/universe-polymorphism.rst | 2 - doc/sphinx/conf.py | 6 ++ doc/sphinx/introduction.rst | 3 - doc/sphinx/language/cic.rst | 3 - doc/sphinx/language/coq-library.rst | 2 - doc/sphinx/language/gallina-extensions.rst | 2 - doc/sphinx/language/module-system.rst | 3 - doc/sphinx/practical-tools/coq-commands.rst | 2 - doc/sphinx/practical-tools/coqide.rst | 2 - doc/sphinx/practical-tools/utilities.rst | 2 - doc/sphinx/preamble.rst | 6 -- doc/sphinx/preamble.tex | 88 ------------------- doc/sphinx/proof-engine/ltac.rst | 3 - doc/sphinx/proof-engine/proof-handling.rst | 1 - .../proof-engine/ssreflect-proof-language.rst | 2 - doc/sphinx/proof-engine/tactics.rst | 3 - doc/sphinx/proof-engine/vernacular-commands.rst | 3 - doc/sphinx/refman-preamble.rst | 98 ++++++++++++++++++++++ doc/sphinx/refman-preamble.sty | 88 +++++++++++++++++++ doc/sphinx/replaces.rst | 89 -------------------- doc/sphinx/user-extensions/syntax-extensions.rst | 2 - 34 files changed, 194 insertions(+), 243 deletions(-) delete mode 100644 doc/sphinx/preamble.rst delete mode 100644 doc/sphinx/preamble.tex create mode 100644 doc/sphinx/refman-preamble.rst create mode 100644 doc/sphinx/refman-preamble.sty delete mode 100644 doc/sphinx/replaces.rst diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index ab4648d577..fbf94fd7da 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -396,7 +396,7 @@ Add either ``undo`` to the first block or ``reset`` to the second block to avoid Abbreviations and macros ------------------------ -Abbreviations and placeholders for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``) are defined in a `separate file `_ included by most chapters of the manual. Some useful LaTeX macros are defined in ``_. +Substitutions for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``), along with some useful LaTeX macros, are defined in a `separate file `_. This file is automatically included in all manual pages. Emacs ----- diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index c333d6e9d5..4ca5171166 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -174,7 +174,7 @@ Add either ``undo`` to the first block or ``reset`` to the second block to avoid Abbreviations and macros ------------------------ -Abbreviations and placeholders for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``) are defined in a `separate file `_ included by most chapters of the manual. Some useful LaTeX macros are defined in ``_. +Substitutions for specially-formatted names (like ``|Cic|``, ``|Coq|``, ``|CoqIDE|``, ``|Ltac|``, and ``|Gallina|``), along with some useful LaTeX macros, are defined in a `separate file `_. This file is automatically included in all manual pages. Emacs ----- diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst index 2cc1f95c08..3e414a714c 100644 --- a/doc/sphinx/addendum/canonical-structures.rst +++ b/doc/sphinx/addendum/canonical-structures.rst @@ -1,4 +1,3 @@ -.. include:: ../replaces.rst .. _canonicalstructures: Canonical Structures diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index e507a224c6..ad6a06d2b0 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _extendedpatternmatching: Extended pattern-matching diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index e3d25cf5cf..4bfa45d54c 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _extraction: Extraction of programs in |OCaml| and Haskell diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index e0babb6c4e..5eba539e03 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. _generalizedrewriting: Generalized rewriting diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index 23cbd76eda..5cb0eaf469 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _implicitcoercions: Implicit Coercions diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst index 0f2d35d044..2cde65dcdc 100644 --- a/doc/sphinx/addendum/miscellaneous-extensions.rst +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _miscellaneousextensions: Miscellaneous extensions diff --git a/doc/sphinx/addendum/nsatz.rst b/doc/sphinx/addendum/nsatz.rst index 9adeca46fc..e7a8c238ac 100644 --- a/doc/sphinx/addendum/nsatz.rst +++ b/doc/sphinx/addendum/nsatz.rst @@ -1,5 +1,3 @@ -.. include:: ../preamble.rst - .. _nsatz_chapter: Nsatz: tactics for proving equalities in integral domains diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst index 8ee8f52227..eb19d57203 100644 --- a/doc/sphinx/addendum/parallel-proof-processing.rst +++ b/doc/sphinx/addendum/parallel-proof-processing.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _asynchronousandparallelproofprocessing: Asynchronous and Parallel Proof Processing diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 78471700be..24247f7bb1 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. this should be just "_program", but refs to it don't work .. _programs: diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 8cb86e2267..58617916c0 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -1,11 +1,9 @@ -.. include:: ../replaces.rst .. |ra| replace:: :math:`\rightarrow_{\beta\delta\iota}` .. |la| replace:: :math:`\leftarrow_{\beta\delta\iota}` .. |eq| replace:: `=`:sub:`(by the main correctness theorem)` .. |re| replace:: ``(PEeval`` `v` `ap`\ ``)`` .. |le| replace:: ``(Pphi_dev`` `v` ``(norm`` `ap`\ ``))`` - .. _theringandfieldtacticfamilies: The ring and field tactic families diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index ab4b4a9824..418014809f 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _typeclasses: Type Classes diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 7e77dea457..706ce1065c 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _polymorphicuniverses: Polymorphic Universes diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 35c08fd806..8b29d1e9f9 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -36,6 +36,12 @@ sys.path.append(os.path.abspath('../../config/')) import coq_config +# -- Prolog --------------------------------------------------------------- + +# Include substitution definitions in all files +with open("refman-preamble.rst") as s: + rst_prolog = s.read() + # -- General configuration ------------------------------------------------ # If your documentation needs a minimal Sphinx version, state it here. diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index 797a9a9714..5bb7bf542c 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -1,6 +1,3 @@ -.. include:: preamble.rst -.. include:: replaces.rst - This document is the Reference Manual of the |Coq| proof assistant. To start using Coq, it is advised to first read a tutorial. Links to several tutorials can be found at diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 13d6e228a6..c8c3e37efb 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. _calculusofinductiveconstructions: diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index 9de30e2190..320448d46e 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _thecoqlibrary: The |Coq| library diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 0fbe7ac70b..ae96a75a94 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _extensionsofgallina: Extensions of |Gallina| diff --git a/doc/sphinx/language/module-system.rst b/doc/sphinx/language/module-system.rst index e6a6736654..15fee91245 100644 --- a/doc/sphinx/language/module-system.rst +++ b/doc/sphinx/language/module-system.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. _themodulesystem: The Module System diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 9498f37c7e..343ca9ed7d 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _thecoqcommands: The |Coq| commands diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index e8fc29dece..9455228e7d 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _coqintegrateddevelopmentenvironment: |Coq| Integrated Development Environment diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index b9a4d2a7bd..5d300c3d6d 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _utilities: --------------------- diff --git a/doc/sphinx/preamble.rst b/doc/sphinx/preamble.rst deleted file mode 100644 index dcbc3322ac..0000000000 --- a/doc/sphinx/preamble.rst +++ /dev/null @@ -1,6 +0,0 @@ -.. 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:: /preamble.tex diff --git a/doc/sphinx/preamble.tex b/doc/sphinx/preamble.tex deleted file mode 100644 index b4fc608e47..0000000000 --- a/doc/sphinx/preamble.tex +++ /dev/null @@ -1,88 +0,0 @@ -\newcommand{\alors}{\textsf{then}} -\newcommand{\alter}{\textsf{alter}} -\newcommand{\as}{\kw{as}} -\newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} -\newcommand{\bool}{\textsf{bool}} -\newcommand{\case}{\kw{case}} -\newcommand{\conc}{\textsf{conc}} -\newcommand{\cons}{\textsf{cons}} -\newcommand{\consf}{\textsf{consf}} -\newcommand{\conshl}{\textsf{cons\_hl}} -\newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} -\newcommand{\emptyf}{\textsf{emptyf}} -\newcommand{\End}{\kw{End}} -\newcommand{\kwend}{\kw{end}} -\newcommand{\EqSt}{\textsf{EqSt}} -\newcommand{\even}{\textsf{even}} -\newcommand{\evenO}{\textsf{even}_\textsf{O}} -\newcommand{\evenS}{\textsf{even}_\textsf{S}} -\newcommand{\false}{\textsf{false}} -\newcommand{\filter}{\textsf{filter}} -\newcommand{\Fix}{\kw{Fix}} -\newcommand{\fix}{\kw{fix}} -\newcommand{\for}{\textsf{for}} -\newcommand{\forest}{\textsf{forest}} -\newcommand{\from}{\textsf{from}} -\newcommand{\Functor}{\kw{Functor}} -\newcommand{\haslength}{\textsf{has\_length}} -\newcommand{\hd}{\textsf{hd}} -\newcommand{\ident}{\textsf{ident}} -\newcommand{\In}{\kw{in}} -\newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} -\newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} -\newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} -\newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} -\newcommand{\injective}{\kw{injective}} -\newcommand{\kw}[1]{\textsf{#1}} -\newcommand{\lb}{\lambda} -\newcommand{\length}{\textsf{length}} -\newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} -\newcommand{\List}{\textsf{list}} -\newcommand{\lra}{\longrightarrow} -\newcommand{\Match}{\kw{match}} -\newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} -\newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} -\newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} -\newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} -\newcommand{\mto}{.\;} -\newcommand{\Nat}{\mathbb{N}} -\newcommand{\nat}{\textsf{nat}} -\newcommand{\Nil}{\textsf{nil}} -\newcommand{\nilhl}{\textsf{nil\_hl}} -\newcommand{\nO}{\textsf{O}} -\newcommand{\node}{\textsf{node}} -\newcommand{\nS}{\textsf{S}} -\newcommand{\odd}{\textsf{odd}} -\newcommand{\oddS}{\textsf{odd}_\textsf{S}} -\newcommand{\ovl}[1]{\overline{#1}} -\newcommand{\Pair}{\textsf{pair}} -\newcommand{\Prod}{\textsf{prod}} -\newcommand{\Prop}{\textsf{Prop}} -\newcommand{\return}{\kw{return}} -\newcommand{\Set}{\textsf{Set}} -\newcommand{\si}{\textsf{if}} -\newcommand{\sinon}{\textsf{else}} -\newcommand{\Sort}{\cal S} -\newcommand{\Str}{\textsf{Stream}} -\newcommand{\Struct}{\kw{Struct}} -\newcommand{\subst}[3]{#1\{#2/#3\}} -\newcommand{\tl}{\textsf{tl}} -\newcommand{\tree}{\textsf{tree}} -\newcommand{\true}{\textsf{true}} -\newcommand{\Type}{\textsf{Type}} -\newcommand{\unfold}{\textsf{unfold}} -\newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} -\newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} -\newcommand{\WF}[2]{{\cal W\!F}(#1)[#2]} -\newcommand{\WFE}[1]{\WF{E}{#1}} -\newcommand{\WFT}[2]{#1[] \vdash {\cal W\!F}(#2)} -\newcommand{\WFTWOLINES}[2]{{\cal W\!F}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} -\newcommand{\with}{\kw{with}} -\newcommand{\WS}[3]{#1[] \vdash #2 <: #3} -\newcommand{\WSE}[2]{\WS{E}{#1}{#2}} -\newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} -\newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} -\newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} -\newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} -\newcommand{\zeroone}[1]{[{#1}]} -\newcommand{\zeros}{\textsf{zeros}} diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 1fc267488c..38fdf243fe 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. _ltac: The tactic language diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index b1e769c571..53294bf8da 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -1,4 +1,3 @@ -.. include:: ../replaces.rst .. _proofhandling: ------------------- diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 8656e5eb3e..361b6e44a5 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _thessreflectprooflanguage: ------------------------------ diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index fb121c82ec..b0b57d00a0 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. _tactics: Tactics diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 584193b9c6..56df535d85 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1,6 +1,3 @@ -.. include:: ../preamble.rst -.. include:: ../replaces.rst - .. _vernacularcommands: Vernacular commands 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`` diff --git a/doc/sphinx/refman-preamble.sty b/doc/sphinx/refman-preamble.sty new file mode 100644 index 0000000000..b4fc608e47 --- /dev/null +++ b/doc/sphinx/refman-preamble.sty @@ -0,0 +1,88 @@ +\newcommand{\alors}{\textsf{then}} +\newcommand{\alter}{\textsf{alter}} +\newcommand{\as}{\kw{as}} +\newcommand{\Assum}[3]{\kw{Assum}(#1)(#2:#3)} +\newcommand{\bool}{\textsf{bool}} +\newcommand{\case}{\kw{case}} +\newcommand{\conc}{\textsf{conc}} +\newcommand{\cons}{\textsf{cons}} +\newcommand{\consf}{\textsf{consf}} +\newcommand{\conshl}{\textsf{cons\_hl}} +\newcommand{\Def}[4]{\kw{Def}(#1)(#2:=#3:#4)} +\newcommand{\emptyf}{\textsf{emptyf}} +\newcommand{\End}{\kw{End}} +\newcommand{\kwend}{\kw{end}} +\newcommand{\EqSt}{\textsf{EqSt}} +\newcommand{\even}{\textsf{even}} +\newcommand{\evenO}{\textsf{even}_\textsf{O}} +\newcommand{\evenS}{\textsf{even}_\textsf{S}} +\newcommand{\false}{\textsf{false}} +\newcommand{\filter}{\textsf{filter}} +\newcommand{\Fix}{\kw{Fix}} +\newcommand{\fix}{\kw{fix}} +\newcommand{\for}{\textsf{for}} +\newcommand{\forest}{\textsf{forest}} +\newcommand{\from}{\textsf{from}} +\newcommand{\Functor}{\kw{Functor}} +\newcommand{\haslength}{\textsf{has\_length}} +\newcommand{\hd}{\textsf{hd}} +\newcommand{\ident}{\textsf{ident}} +\newcommand{\In}{\kw{in}} +\newcommand{\Ind}[4]{\kw{Ind}[#2](#3:=#4)} +\newcommand{\ind}[3]{\kw{Ind}~[#1]\left(#2\mathrm{~:=~}#3\right)} +\newcommand{\Indp}[5]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)} +\newcommand{\Indpstr}[6]{\kw{Ind}_{#5}(#1)[#2](#3:=#4)/{#6}} +\newcommand{\injective}{\kw{injective}} +\newcommand{\kw}[1]{\textsf{#1}} +\newcommand{\lb}{\lambda} +\newcommand{\length}{\textsf{length}} +\newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3} +\newcommand{\List}{\textsf{list}} +\newcommand{\lra}{\longrightarrow} +\newcommand{\Match}{\kw{match}} +\newcommand{\Mod}[3]{{\kw{Mod}}({#1}:{#2}\,\zeroone{:={#3}})} +\newcommand{\ModA}[2]{{\kw{ModA}}({#1}=={#2})} +\newcommand{\ModS}[2]{{\kw{Mod}}({#1}:{#2})} +\newcommand{\ModType}[2]{{\kw{ModType}}({#1}:={#2})} +\newcommand{\mto}{.\;} +\newcommand{\Nat}{\mathbb{N}} +\newcommand{\nat}{\textsf{nat}} +\newcommand{\Nil}{\textsf{nil}} +\newcommand{\nilhl}{\textsf{nil\_hl}} +\newcommand{\nO}{\textsf{O}} +\newcommand{\node}{\textsf{node}} +\newcommand{\nS}{\textsf{S}} +\newcommand{\odd}{\textsf{odd}} +\newcommand{\oddS}{\textsf{odd}_\textsf{S}} +\newcommand{\ovl}[1]{\overline{#1}} +\newcommand{\Pair}{\textsf{pair}} +\newcommand{\Prod}{\textsf{prod}} +\newcommand{\Prop}{\textsf{Prop}} +\newcommand{\return}{\kw{return}} +\newcommand{\Set}{\textsf{Set}} +\newcommand{\si}{\textsf{if}} +\newcommand{\sinon}{\textsf{else}} +\newcommand{\Sort}{\cal S} +\newcommand{\Str}{\textsf{Stream}} +\newcommand{\Struct}{\kw{Struct}} +\newcommand{\subst}[3]{#1\{#2/#3\}} +\newcommand{\tl}{\textsf{tl}} +\newcommand{\tree}{\textsf{tree}} +\newcommand{\true}{\textsf{true}} +\newcommand{\Type}{\textsf{Type}} +\newcommand{\unfold}{\textsf{unfold}} +\newcommand{\WEV}[3]{\mbox{$#1[] \vdash #2 \lra #3$}} +\newcommand{\WEVT}[3]{\mbox{$#1[] \vdash #2 \lra$}\\ \mbox{$ #3$}} +\newcommand{\WF}[2]{{\cal W\!F}(#1)[#2]} +\newcommand{\WFE}[1]{\WF{E}{#1}} +\newcommand{\WFT}[2]{#1[] \vdash {\cal W\!F}(#2)} +\newcommand{\WFTWOLINES}[2]{{\cal W\!F}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}} +\newcommand{\with}{\kw{with}} +\newcommand{\WS}[3]{#1[] \vdash #2 <: #3} +\newcommand{\WSE}[2]{\WS{E}{#1}{#2}} +\newcommand{\WT}[4]{#1[#2] \vdash #3 : #4} +\newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}} +\newcommand{\WTEG}[2]{\WTE{\Gamma}{#1}{#2}} +\newcommand{\WTM}[3]{\WT{#1}{}{#2}{#3}} +\newcommand{\zeroone}[1]{[{#1}]} +\newcommand{\zeros}{\textsf{zeros}} diff --git a/doc/sphinx/replaces.rst b/doc/sphinx/replaces.rst deleted file mode 100644 index 28a04f90ce..0000000000 --- a/doc/sphinx/replaces.rst +++ /dev/null @@ -1,89 +0,0 @@ -.. 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`` diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 4c0e85bdd4..0236f19490 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1,5 +1,3 @@ -.. include:: ../replaces.rst - .. _syntaxextensionsandinterpretationscopes: Syntax extensions and interpretation scopes -- cgit v1.2.3