diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/README.md | 14 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 81 |
3 files changed, 39 insertions, 61 deletions
diff --git a/doc/README.md b/doc/README.md index 6c6e1f01fb..3e70bc443d 100644 --- a/doc/README.md +++ b/doc/README.md @@ -9,7 +9,7 @@ The Coq documentation includes The documentation of the latest released version is available on the Coq web site at [coq.inria.fr/documentation](http://coq.inria.fr/documentation). -Additionnally, you can view the documentation for the current master version at +Additionally, you can view the documentation for the current master version at <https://gitlab.com/coq/coq/-/jobs/artifacts/master/file/_install_ci/share/doc/coq/sphinx/html/index.html?job=documentation>. The reference manual is written is reStructuredText and compiled @@ -89,6 +89,18 @@ Alternatively, you can use some specific targets: Also note the `-with-doc yes` option of `./configure` to enable the build of the documentation as part of the default make target. +If you're editing Sphinx documentation, set SPHINXWARNERROR to 0 +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 SPINXWARNERROR=0` + +- ~~~ + export SPHINXWARNERROR=0 + ⋮ + make sphinx + ~~~ Installation ------------ diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index b49d0f0504..fe2124502a 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -315,6 +315,9 @@ Navigation in the proof tree .. _curly-braces: +.. index:: { + } + .. cmd:: %{ %| %} The command ``{`` (without a terminating period) focuses on the first @@ -369,7 +372,7 @@ Navigation in the proof tree Brackets are used to focus on a single goal given either by its position or by its name if it has one. - .. seealso:: The error messages about bullets below. + .. seealso:: The error messages about bullets below. .. _bullets: diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 8a2fc3996a..be30f69704 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -2522,7 +2522,8 @@ After the :token:`i_pattern`, a list of binders is allowed. .. coqtop:: reset - From Coq Require Import ssreflect Omega. + From Coq Require Import ssreflect. + From Coq Require Import Omega. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -2552,12 +2553,9 @@ copying the goal itself. .. example:: - .. coqtop:: reset + .. coqtop:: none - From Coq Require Import ssreflect. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. + Abort All. .. coqtop:: all @@ -2581,12 +2579,9 @@ context entry name. .. example:: - .. coqtop:: reset + .. coqtop:: none - From Coq Require Import ssreflect Omega. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. + Abort All. Set Printing Depth 15. .. coqtop:: all @@ -2601,20 +2596,13 @@ context entry name. Note that the sub-term produced by ``omega`` is in general huge and uninteresting, and hence one may want to hide it. For this purpose the ``[: name ]`` intro pattern and the tactic -``abstract`` (see page :ref:`abstract_ssr`) are provided. +``abstract`` (see :ref:`abstract_ssr`) are provided. .. example:: - .. coqtop:: reset - - From Coq Require Import ssreflect Omega. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. + .. coqtop:: none - Inductive Ord n := Sub x of x < n. - Notation "'I_ n" := (Ord n) (at level 8, n at level 2, format "''I_' n"). - Arguments Sub {_} _ _. + Abort All. .. coqtop:: all @@ -2629,16 +2617,9 @@ with have and an explicit term, they must be used as follows: .. example:: - .. coqtop:: reset - - From Coq Require Import ssreflect Omega. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. + .. coqtop:: none - Inductive Ord n := Sub x of x < n. - Notation "'I_ n" := (Ord n) (at level 8, n at level 2, format "''I_' n"). - Arguments Sub {_} _ _. + Abort All. .. coqtop:: all @@ -2659,16 +2640,9 @@ makes use of it). .. example:: - .. coqtop:: reset + .. coqtop:: none - From Coq Require Import ssreflect Omega. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. - - Inductive Ord n := Sub x of x < n. - Notation "'I_ n" := (Ord n) (at level 8, n at level 2, format "''I_' n"). - Arguments Sub {_} _ _. + Abort All. .. coqtop:: all @@ -2685,12 +2659,9 @@ The have tactic and type classes resolution Since |SSR| 1.5 the have tactic behaves as follows with respect to type classes inference. - .. coqtop:: reset + .. coqtop:: none - From Coq Require Import ssreflect Omega. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. + Abort All. Axiom ty : Type. Axiom t : ty. @@ -2766,12 +2737,9 @@ The ``have`` modifier can follow the ``suff`` tactic. .. example:: - .. coqtop:: reset + .. coqtop:: none - From Coq Require Import ssreflect Omega. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. + Abort All. Axioms G P : Prop. .. coqtop:: all @@ -2839,12 +2807,9 @@ are unique. .. example:: - .. coqtop:: reset + .. coqtop:: none - From Coq Require Import ssreflect Omega. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. + Abort All. .. coqtop:: all @@ -2935,12 +2900,10 @@ illustrated in the following example. the pattern ``id (addx x)``, that would produce the following first subgoal - .. coqtop:: reset + .. coqtop:: none - From Coq Require Import ssreflect Omega. - Set Implicit Arguments. - Unset Strict Implicit. - Unset Printing Implicit Defensive. + Abort All. + From Coq Require Import Omega. Section Test. Variable x : nat. Definition addx z := z + x. |