aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
Diffstat (limited to 'doc')
-rw-r--r--doc/README.md11
-rw-r--r--doc/sphinx/README.rst37
-rw-r--r--doc/sphinx/addendum/micromega.rst13
-rw-r--r--doc/sphinx/addendum/omega.rst7
-rwxr-xr-xdoc/sphinx/conf.py4
-rw-r--r--doc/sphinx/credits-contents.rst (renamed from doc/sphinx/credits.rst)0
-rw-r--r--doc/sphinx/credits-wrapper.latex.rst3
-rw-r--r--doc/sphinx/credits.html.rst (renamed from doc/sphinx/credits-wrapper.html.rst)2
-rw-r--r--doc/sphinx/credits.latex.rst3
-rw-r--r--doc/sphinx/index.html.rst14
-rw-r--r--doc/sphinx/index.latex.rst7
-rw-r--r--doc/sphinx/introduction.rst5
-rw-r--r--doc/tools/coqrst/coqdomain.py26
13 files changed, 67 insertions, 65 deletions
diff --git a/doc/README.md b/doc/README.md
index 1461fa2e2c..3db1261656 100644
--- a/doc/README.md
+++ b/doc/README.md
@@ -88,8 +88,11 @@ Alternatively, you can use some specific targets:
- `make doc-html`
to produce all HTML documents
-- `make sphinx`
- to produce the HTML and PDF versions of the reference manual
+- `make refman`
+ to produce the HTML and PDF versions of the reference manual
+
+- `make refman-{html,pdf}`
+ to produce only one format of the reference manual
- `make stdlib`
to produce all formats of the Coq standard library
@@ -103,12 +106,12 @@ to avoid treating Sphinx warnings as errors. Otherwise, Sphinx quits
upon detecting the first warning. You can set this on the Sphinx `make`
command line or as an environment variable:
-- `make sphinx SPHINXWARNERROR=0`
+- `make refman SPHINXWARNERROR=0`
- ~~~
export SPHINXWARNERROR=0
⋮
- make sphinx
+ make refman
~~~
Installation
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst
index c1f3f7b4d0..4ad952bdfb 100644
--- a/doc/sphinx/README.rst
+++ b/doc/sphinx/README.rst
@@ -114,32 +114,23 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica
Raised if :n:`@tactic` does not fully solve the goal.
-``.. flag::`` :black_nib: A Coq flag (i.e a binary-valued setting).
+``.. flag::`` :black_nib: A Coq flag (i.e. a boolean setting).
Example::
.. flag:: Nonrecursive Elimination Schemes
- This option controls whether types declared with the keywords
- :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the
+ Controls whether types declared with the keywords
+ :cmd:`Variant` and :cmd:`Record` get an automatic declaration of
induction principles.
-``.. opt::`` :black_nib: A Coq option (with a string or numeric value; use "flag" for binary options)
+``.. opt::`` :black_nib: A Coq option (a setting with non-boolean value, e.g. a string or numeric value).
Example::
- .. opt:: Printing Width @num
- :name: Printing Width
+ .. opt:: Hyps Limit @num
+ :name Hyps Limit
- This command sets which left-aligned part of the width of the screen is used
- for display. At the time of writing this documentation, the default value
- is 78.
-
-``.. table::`` :black_nib: A Coq table (i.e a setting whose value is a set).
- Example::
-
- .. table:: Search Blacklist @string
- :name: Search Blacklist
-
- This table controls ...
+ Controls the maximum number of hypotheses displayed in goals after
+ application of a tactic.
``.. prodn::`` A grammar production.
This is useful if you intend to document individual grammar productions.
@@ -159,6 +150,14 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica
.. prodn:: term += let: @pattern := @term in @term
.. prodn:: occ_switch ::= { {? + %| - } {* @num } }
+``.. table::`` :black_nib: A Coq table, i.e. a setting that is a set of values.
+ Example::
+
+ .. table:: Search Blacklist @string
+ :name: Search Blacklist
+
+ Controls ...
+
``.. tacn::`` :black_nib: A tactic, or a tactic notation.
Example::
@@ -293,7 +292,9 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo
\WTEG{\forall~x:T,U}{\Prop}
``.. preamble::`` A reST directive to include a TeX file.
- Mostly useful to let MathJax know about `\def`s and `\newcommand`s.
+ Mostly useful to let MathJax know about `\def`s and `\newcommand`s. The
+ contents of the TeX file are wrapped in a math environment, as MathJax
+ doesn't process LaTeX definitions otherwise.
Usage::
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index d03a31c044..3b9760f586 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -112,11 +112,11 @@ and checked to be :math:`-1`.
.. tacn:: lia
:name: lia
-This tactic offers an alternative to the :tacn:`omega` and :tacn:`romega`
-tactics. Roughly speaking, the deductive power of lia is the combined deductive
-power of :tacn:`ring_simplify` and :tacn:`omega`. However, it solves linear
-goals that :tacn:`omega` and :tacn:`romega` do not solve, such as the following
-so-called *omega nightmare* :cite:`TheOmegaPaper`.
+ This tactic offers an alternative to the :tacn:`omega` tactic. Roughly
+ speaking, the deductive power of lia is the combined deductive power of
+ :tacn:`ring_simplify` and :tacn:`omega`. However, it solves linear goals
+ that :tacn:`omega` does not solve, such as the following so-called *omega
+ nightmare* :cite:`TheOmegaPaper`.
.. coqtop:: in
@@ -124,8 +124,7 @@ so-called *omega nightmare* :cite:`TheOmegaPaper`.
27 <= 11 * x + 13 * y <= 45 ->
-10 <= 7 * x - 9 * y <= 4 -> False.
-The estimation of the relative efficiency of :tacn:`lia` *vs* :tacn:`omega` and
-:tacn:`romega` is under evaluation.
+The estimation of the relative efficiency of :tacn:`lia` *vs* :tacn:`omega` is under evaluation.
High level view of `lia`
~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst
index 828505b850..03d4f148e3 100644
--- a/doc/sphinx/addendum/omega.rst
+++ b/doc/sphinx/addendum/omega.rst
@@ -23,13 +23,6 @@ Description of ``omega``
If the tactic cannot solve the goal, it fails with an error message.
In any case, the computation eventually stops.
-.. tacv:: romega
- :name: romega
-
- .. deprecated:: 8.9
-
- Use :tacn:`lia` instead.
-
Arithmetical goals recognized by ``omega``
------------------------------------------
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index b43d5fb6f0..71f01cbb17 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -106,7 +106,7 @@ def setup(app):
master_doc = "index"
# General information about the project.
-project = 'The Coq Reference Manual'
+project = 'Coq'
copyright = '1999-2018, Inria'
author = 'The Coq Development Team'
@@ -335,7 +335,7 @@ latex_additional_files = [
"_static/coqnotations.sty"
]
-latex_documents = [('index', 'CoqRefMan.tex', project, author, 'manual')]
+latex_documents = [('index', 'CoqRefMan.tex', 'The Coq Reference Manual', author, 'manual')]
# The name of an image file (relative to this directory) to place at the top of
# the title page.
diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits-contents.rst
index 212f0a65b0..212f0a65b0 100644
--- a/doc/sphinx/credits.rst
+++ b/doc/sphinx/credits-contents.rst
diff --git a/doc/sphinx/credits-wrapper.latex.rst b/doc/sphinx/credits-wrapper.latex.rst
deleted file mode 100644
index 9f7dd49af8..0000000000
--- a/doc/sphinx/credits-wrapper.latex.rst
+++ /dev/null
@@ -1,3 +0,0 @@
-.. _credits:
-
-.. include:: credits.rst
diff --git a/doc/sphinx/credits-wrapper.html.rst b/doc/sphinx/credits.html.rst
index 2d35a12dc2..0b2b1c6ad1 100644
--- a/doc/sphinx/credits-wrapper.html.rst
+++ b/doc/sphinx/credits.html.rst
@@ -4,4 +4,4 @@
Credits
-------
-.. include:: credits.rst
+.. include:: credits-contents.rst
diff --git a/doc/sphinx/credits.latex.rst b/doc/sphinx/credits.latex.rst
new file mode 100644
index 0000000000..39101f9d52
--- /dev/null
+++ b/doc/sphinx/credits.latex.rst
@@ -0,0 +1,3 @@
+.. _credits:
+
+.. include:: credits-contents.rst
diff --git a/doc/sphinx/index.html.rst b/doc/sphinx/index.html.rst
index 9d90857061..cf12b57414 100644
--- a/doc/sphinx/index.html.rst
+++ b/doc/sphinx/index.html.rst
@@ -1,11 +1,8 @@
-==========================
- The Coq Reference Manual
-==========================
-
.. _introduction:
+==========================
Introduction
-------------
+==========================
.. include:: introduction.rst
@@ -28,7 +25,7 @@ Table of contents
:caption: Preamble
self
- credits-wrapper
+ credits
.. toctree::
:caption: The language
@@ -89,3 +86,8 @@ License
-------
.. include:: license.rst
+
+.. [#PG] Proof-General is available at https://proofgeneral.github.io/.
+ Optionally, you can enhance it with the minor mode
+ Company-Coq :cite:`Pit16`
+ (see https://github.com/cpitclaudel/company-coq).
diff --git a/doc/sphinx/index.latex.rst b/doc/sphinx/index.latex.rst
index 0f2f7b4897..af757f8746 100644
--- a/doc/sphinx/index.latex.rst
+++ b/doc/sphinx/index.latex.rst
@@ -7,10 +7,15 @@ Introduction
.. include:: introduction.rst
+.. [#PG] Proof-General is available at https://proofgeneral.github.io/.
+ Optionally, you can enhance it with the minor mode
+ Company-Coq :cite:`Pit16`
+ (see https://github.com/cpitclaudel/company-coq).
+
Credits
-------
-.. include:: credits-wrapper.rst
+.. include:: credits.rst
License
-------
diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst
index b8d2f6b6dc..5bb7bf542c 100644
--- a/doc/sphinx/introduction.rst
+++ b/doc/sphinx/introduction.rst
@@ -35,11 +35,6 @@ are processed from a file.
The `coqtop` read-eval-print-loop can also be used directly, for debugging
purposes.
- .. [#PG] Proof-General is available at https://proofgeneral.github.io/.
- Optionally, you can enhance it with the minor mode
- Company-Coq :cite:`Pit16`
- (see https://github.com/cpitclaudel/company-coq).
-
- The compiled mode acts as a proof checker taking a file containing a
whole development in order to ensure its correctness. Moreover,
|Coq|’s compiler provides an output file containing a compact
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 7992c10abb..edf4e6ec9d 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -333,14 +333,15 @@ class TacticNotationVariantObject(TacticNotationObject):
annotation = "Variant"
class OptionObject(NotationObject):
- """A Coq option.
+ """A Coq option (a setting with non-boolean value, e.g. a string or numeric value).
Example::
.. opt:: Hyps Limit @num
+ :name Hyps Limit
- This option controls the maximum number of hypotheses displayed in goals after
- the application of a tactic.
+ Controls the maximum number of hypotheses displayed in goals after
+ application of a tactic.
"""
subdomain = "opt"
index_suffix = "(opt)"
@@ -351,14 +352,14 @@ class OptionObject(NotationObject):
class FlagObject(NotationObject):
- """A Coq flag, i.e. a boolean Option.
+ """A Coq flag (i.e. a boolean setting).
Example::
.. flag:: Nonrecursive Elimination Schemes
- This flag controls whether types declared with the keywords
- :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the
+ Controls whether types declared with the keywords
+ :cmd:`Variant` and :cmd:`Record` get an automatic declaration of
induction principles.
"""
subdomain = "flag"
@@ -374,9 +375,10 @@ class TableObject(NotationObject):
Example::
- .. table:: Search Blacklist
+ .. table:: Search Blacklist @string
+ :name: Search Blacklist
- This table controls ...
+ Controls ...
"""
subdomain = "table"
index_suffix = "(table)"
@@ -664,7 +666,9 @@ class ExampleDirective(BaseAdmonition):
class PreambleDirective(Directive):
r"""A reST directive to include a TeX file.
- Mostly useful to let MathJax know about `\def`s and `\newcommand`s.
+ Mostly useful to let MathJax know about `\def`s and `\newcommand`s. The
+ contents of the TeX file are wrapped in a math environment, as MathJax
+ doesn't process LaTeX definitions otherwise.
Usage::
@@ -691,7 +695,7 @@ class PreambleDirective(Directive):
with open(abs_fname, encoding="utf-8") as ltx:
latex = ltx.read()
- node = make_math_node(latex, env.docname, nowrap=True)
+ node = make_math_node(latex, env.docname, nowrap=False)
node['classes'] = ["math-preamble"]
set_source_info(self, node)
return [node]
@@ -1192,6 +1196,6 @@ def setup(app):
# contents of ``env.domaindata['coq']`` change. See
# `https://github.com/sphinx-doc/sphinx/issues/4460`.
meta = { "version": "0.1",
- "env_version": 1,
+ "env_version": 2,
"parallel_read_safe": True }
return meta
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 23:19:55 +0000