aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/sphinx
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-05-14 13:43:41 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-05-14 13:43:41 +0200
commit9e3989f949c1e3f20031d9af5a7bc89d97f5a951 (patch)
treea3bc0f6a7f80840f84109460a3169726ffffe590 /doc/sphinx
parent4094a8c2cac668db112fc84f5d1b287eacbf6700 (diff)
parent805d78d12443d9df646362c024bfa83466c27fdd (diff)
Merge PR #7374: [sphinx] More fatal warnings.
Diffstat (limited to 'doc/sphinx')
-rw-r--r--doc/sphinx/addendum/generalized-rewriting.rst3
-rw-r--r--doc/sphinx/addendum/implicit-coercions.rst9
-rw-r--r--doc/sphinx/addendum/omega.rst5
-rw-r--r--doc/sphinx/language/gallina-extensions.rst65
-rw-r--r--doc/sphinx/language/gallina-specification-language.rst2
-rw-r--r--doc/sphinx/proof-engine/ltac.rst3
-rw-r--r--doc/sphinx/proof-engine/tactics.rst59
-rw-r--r--doc/sphinx/proof-engine/vernacular-commands.rst31
-rw-r--r--doc/sphinx/user-extensions/proof-schemes.rst1
-rw-r--r--doc/sphinx/user-extensions/syntax-extensions.rst5
10 files changed, 106 insertions, 77 deletions
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst
index f5237e4fb..e10e16c10 100644
--- a/doc/sphinx/addendum/generalized-rewriting.rst
+++ b/doc/sphinx/addendum/generalized-rewriting.rst
@@ -599,6 +599,7 @@ Notice that the syntax is not completely backward compatible since the
identifier was not required.
.. cmd:: Add Morphism f : @ident
+ :name: Add Morphism
The latter command also is restricted to the declaration of morphisms
without parameters. It is not fully backward compatible since the
@@ -616,7 +617,7 @@ the same signature. Finally, the :tacn:`replace` and :tacn:`rewrite` tactics can
used to replace terms in contexts that were refused by the old
implementation. As discussed in the next section, the semantics of the
new :tacn:`setoid_rewrite` tactic differs slightly from the old one and
-tacn:`rewrite`.
+:tacn:`rewrite`.
Extensions
diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst
index 5f8c06484..152f4f655 100644
--- a/doc/sphinx/addendum/implicit-coercions.rst
+++ b/doc/sphinx/addendum/implicit-coercions.rst
@@ -263,9 +263,12 @@ Activating the Printing of Coercions
.. cmd:: Add Printing Coercion @qualid
- This command forces coercion denoted by :n:`@qualid` to be printed. To skip
- the printing of coercion :n:`@qualid`, use :cmd:`Remove Printing Coercion`. By
- default, a coercion is never printed.
+ This command forces coercion denoted by :n:`@qualid` to be printed.
+ By default, a coercion is never printed.
+
+.. cmd:: Remove Printing Coercion @qualid
+
+ Use this command, to skip the printing of coercion :n:`@qualid`.
.. _coercions-classes-as-records:
diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst
index 009efd0d2..80ce01620 100644
--- a/doc/sphinx/addendum/omega.rst
+++ b/doc/sphinx/addendum/omega.rst
@@ -26,6 +26,11 @@ solvable. This is the restriction meant by "Presburger arithmetic".
If the tactic cannot solve the goal, it fails with an error message.
In any case, the computation eventually stops.
+.. tacv:: romega
+ :name: romega
+
+ To be documented.
+
Arithmetical goals recognized by ``omega``
------------------------------------------
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 8746897e7..53b993edd 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -1175,52 +1175,53 @@ component is equal ``nat`` and hence ``M1.T`` as specified.
If `qualid` denotes a valid basic module (i.e. its module type is a
signature), makes its components available by their short names.
-.. example::
+ .. example::
- .. coqtop:: reset all
+ .. coqtop:: reset all
- Module Mod.
+ Module Mod.
- Definition T:=nat.
+ Definition T:=nat.
- Check T.
+ Check T.
- End Mod.
+ End Mod.
- Check Mod.T.
+ Check Mod.T.
- Fail Check T.
+ Fail Check T.
- Import Mod.
+ Import Mod.
- Check T.
+ Check T.
-Some features defined in modules are activated only when a module is
-imported. This is for instance the case of notations (see :ref:`Notations`).
+ Some features defined in modules are activated only when a module is
+ imported. This is for instance the case of notations (see :ref:`Notations`).
-Declarations made with the Local flag are never imported by theImport
-command. Such declarations are only accessible through their fully
-qualified name.
+ Declarations made with the ``Local`` flag are never imported by the :cmd:`Import`
+ command. Such declarations are only accessible through their fully
+ qualified name.
-.. example::
+ .. example::
- .. coqtop:: all
+ .. coqtop:: all
- Module A.
+ Module A.
- Module B.
+ Module B.
- Local Definition T := nat.
+ Local Definition T := nat.
- End B.
+ End B.
- End A.
+ End A.
- Import A.
+ Import A.
- Fail Check B.T.
+ Fail Check B.T.
.. cmdv:: Export @qualid
+ :name: Export
When the module containing the command Export qualid
is imported, qualid is imported as well.
@@ -1231,16 +1232,17 @@ qualified name.
.. cmd:: Print Module @ident
- Prints the module type and (optionally) the body of the module `ident`.
+ Prints the module type and (optionally) the body of the module :n:`@ident`.
.. cmd:: Print Module Type @ident
- Prints the module type corresponding to `ident`.
+ Prints the module type corresponding to :n:`@ident`.
.. opt:: Short Module Printing
- This option (off by default) disables the printing of the types of fields,
- leaving only their names, for the commands ``Print Module`` and ``Print Module Type``.
+ This option (off by default) disables the printing of the types of fields,
+ leaving only their names, for the commands :cmd:`Print Module` and
+ :cmd:`Print Module Type`.
Libraries and qualified names
---------------------------------
@@ -1510,9 +1512,8 @@ implicitly applied to the implicit arguments it is waiting for: one
says that the implicit argument is maximally inserted.
Each implicit argument can be declared to have to be inserted maximally or non
-maximally. This can be governed argument per argument by the command ``Implicit
-Arguments`` (see Section :ref:`declare-implicit-args`) or globally by the
-:opt:`Maximal Implicit Insertion` option.
+maximally. This can be governed argument per argument by the command
+:cmd:`Arguments (implicits)` or globally by the :opt:`Maximal Implicit Insertion` option.
See also :ref:`displaying-implicit-args`.
@@ -1565,7 +1566,7 @@ absent in every situation but still be able to specify it if needed:
The syntax is supported in all top-level definitions:
-``Definition``, ``Fixpoint``, ``Lemma`` and so on. For (co-)inductive datatype
+:cmd:`Definition`, :cmd:`Fixpoint`, :cmd:`Lemma` and so on. For (co-)inductive datatype
declarations, the semantics are the following: an inductive parameter
declared as an implicit argument need not be repeated in the inductive
definition but will become implicit for the constructors of the
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 46e684b12..39735a6ed 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -609,6 +609,7 @@ of any section is equivalent to using ``Local Parameter``.
Adds blocks of variables with different specifications.
.. cmdv:: Variables {+ ( {+ @ident } : @term) }
+ :name: Variables
.. cmdv:: Hypothesis {+ ( {+ @ident } : @term) }
:name: Hypothesis
@@ -672,6 +673,7 @@ Section :ref:`typing-rules`.
You have to explicitly give their fully qualified name to refer to them.
.. cmdv:: Example @ident := @term
+ :name: Example
.. cmdv:: Example @ident : @term := @term
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index c5ee724ca..2b128b98f 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -245,7 +245,7 @@ focused goals with:
:name: ... : ... (goal selector)
We can also use selectors as a tactical, which allows to use them nested
- in a tactic expression, by using the keyword :tacn:`only`:
+ in a tactic expression, by using the keyword ``only``:
.. tacv:: only selector : expr
:name: only ... : ...
@@ -826,6 +826,7 @@ We can make pattern matching on goals using the following expression:
.. we should provide the full grammar here
.. tacn:: match goal with {+| {+ hyp} |- @cpattern => @expr } | _ => @expr end
+ :name: match goal
If each hypothesis pattern :n:`hyp`\ :sub:`1,i`, with i=1,...,m\ :sub:`1` is
matched (non-linear first-order unification) by an hypothesis of the
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 20a362c4c..0318bddde 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -648,6 +648,7 @@ be applied or the goal is not head-reducible.
.. exn:: @ident is already used.
.. tacv:: intros
+ :name: intros
This repeats ``intro`` until it meets the head-constant. It never
reduces head-constants and it never fails.
@@ -714,7 +715,7 @@ be applied or the goal is not head-reducible.
These tactics behave as previously but naming the introduced hypothesis
:n:`@ident`. It is equivalent to :n:`intro @ident` followed by the
- appropriate call to move (see :tacn:`move ... after`).
+ appropriate call to ``move`` (see :tacn:`move ... after ...`).
.. tacn:: intros @intro_pattern_list
:name: intros ...
@@ -917,7 +918,7 @@ the inverse of :tacn:`intro`.
depend on it.
.. tacn:: move @ident after @ident
- :name: move .. after ...
+ :name: move ... after ...
This moves the hypothesis named :n:`@ident` in the local context after the
hypothesis named :n:`@ident`, where “after” is in reference to the
@@ -2148,7 +2149,7 @@ See also: :ref:`advanced-recursive-functions`
:n:`dependent inversion_clear @ident`.
.. tacv:: dependent inversion @ident with @term
- :name: dependent inversion ...
+ :name: dependent inversion ... with ...
This variant allows you to specify the generalization of the goal. It is
useful when the system fails to generalize the goal automatically. If
@@ -2163,7 +2164,7 @@ See also: :ref:`advanced-recursive-functions`
.. tacv:: dependent inversion_clear @ident with @term
- Like :tacn:`dependent inversion ...` with but clears :n:`@ident` from the
+ Like :tacn:`dependent inversion ... with ...` with but clears :n:`@ident` from the
local context.
.. tacv:: dependent inversion_clear @ident as @intro_pattern with @term
@@ -3193,7 +3194,7 @@ can solve such a goal:
Goal forall P:nat -> Prop, P 0 -> exists n, P n.
eauto.
-Note that :tacn:`ex_intro` should be declared as a hint.
+Note that ``ex_intro`` should be declared as a hint.
.. tacv:: {? info_}eauto {? @num} {? using {+ @lemma}} {? with {+ @ident}}
@@ -3444,6 +3445,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
Declares each :n:`@ident` as a transparent or opaque constant.
.. cmdv:: Hint Extern @num {? @pattern} => tactic
+ :name: Hint Extern
This hint type is to extend :tacn:`auto` with tactics other than :tacn:`apply` and
:tacn:`unfold`. For that, we must specify a cost, an optional :n:`@pattern` and a
@@ -3664,6 +3666,7 @@ option which accepts three flags allowing for a fine-grained handling of
non-imported hints.
.. opt:: Loose Hint Behavior %( "Lax" %| "Warn" %| "Strict" %)
+ :name: Loose Hint Behavior
This option accepts three values, which control the behavior of hints w.r.t.
:cmd:`Import`:
@@ -3808,14 +3811,15 @@ some incompatibilities.
.. tacv:: intuition
- Is equivalent to :g:`intuition auto with *`.
+ Is equivalent to :g:`intuition auto with *`.
.. tacv:: dintuition
+ :name: dintuition
- While :tacn:`intuition` recognizes inductively defined connectives
- isomorphic to the standard connective ``and, prod, or, sum, False,
- Empty_set, unit, True``, :tacn:`dintuition` recognizes also all inductive
- types with one constructors and no indices, i.e. record-style connectives.
+ While :tacn:`intuition` recognizes inductively defined connectives
+ isomorphic to the standard connective ``and``, ``prod``, ``or``, ``sum``, ``False``,
+ ``Empty_set``, ``unit``, ``True``, :tacn:`dintuition` recognizes also all inductive
+ types with one constructors and no indices, i.e. record-style connectives.
.. opt:: Intuition Negation Unfolding
@@ -3844,11 +3848,14 @@ first- order reasoning, written by Pierre Corbineau. It is not restricted to
usual logical connectives but instead may reason about any first-order class
inductive definition.
-.. opt:: Firstorder Solver
+.. opt:: Firstorder Solver @tactic
The default tactic used by :tacn:`firstorder` when no rule applies is
- :g:`auto with *`, it can be reset locally or globally using this option and
- printed using :cmd:`Print Firstorder Solver`.
+ :g:`auto with *`, it can be reset locally or globally using this option.
+
+ .. cmd:: Print Firstorder Solver
+
+ Prints the default tactic used by :tacn:`firstorder` when no rule applies.
.. tacv:: firstorder @tactic
@@ -4011,8 +4018,8 @@ solved by :tacn:`f_equal`.
:name: reflexivity
This tactic applies to a goal that has the form :g:`t=u`. It checks that `t`
-and `u` are convertible and then solves the goal. It is equivalent to apply
-:tacn:`refl_equal`.
+and `u` are convertible and then solves the goal. It is equivalent to
+``apply refl_equal``.
.. exn:: The conclusion is not a substitutive equation.
@@ -4104,7 +4111,7 @@ symbol :g:`=`.
:n:`intro @ident; simplify_eq @ident`.
.. tacn:: dependent rewrite -> @ident
- :name: dependent rewrite
+ :name: dependent rewrite ->
This tactic applies to any goal. If :n:`@ident` has type
:g:`(existT B a b)=(existT B a' b')` in the local context (i.e. each
@@ -4115,6 +4122,7 @@ symbol :g:`=`.
:tacn:`injection` and :tacn:`inversion` tactics.
.. tacv:: dependent rewrite <- @ident
+ :name: dependent rewrite <-
Analogous to :tacn:`dependent rewrite ->` but uses the equality from right to
left.
@@ -4374,19 +4382,20 @@ This tactics reverses the list of the focused goals.
unification, or they can be called back into focus with the command
:cmd:`Unshelve`.
-.. tacv:: shelve_unifiable
+ .. tacv:: shelve_unifiable
+ :name: shelve_unifiable
- Shelves only the goals under focus that are mentioned in other goals.
- Goals that appear in the type of other goals can be solved by unification.
+ Shelves only the goals under focus that are mentioned in other goals.
+ Goals that appear in the type of other goals can be solved by unification.
-.. example::
+ .. example::
- .. coqtop:: all reset
+ .. coqtop:: all reset
- Goal exists n, n=0.
- refine (ex_intro _ _ _).
- all:shelve_unifiable.
- reflexivity.
+ Goal exists n, n=0.
+ refine (ex_intro _ _ _).
+ all: shelve_unifiable.
+ reflexivity.
.. cmd:: Unshelve
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 7ba103b22..c37233734 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -360,6 +360,7 @@ Requests to the environment
Search (?x * _ + ?x * _)%Z outside OmegaLemmas.
.. cmdv:: SearchAbout
+ :name: SearchAbout
.. deprecated:: 8.5
@@ -416,7 +417,7 @@ Requests to the environment
current goal (if any) and theorems of the current context whose
statement’s conclusion or last hypothesis and conclusion matches the
expressionterm where holes in the latter are denoted by `_`.
- It is a variant of Search @term_pattern that does not look for subterms
+ It is a variant of :n:`Search @term_pattern` that does not look for subterms
but searches for statements whose conclusion has exactly the expected
form, or whose statement finishes by the given series of
hypothesis/conclusion.
@@ -625,6 +626,7 @@ file is a particular case of module called *library file*.
.. cmdv:: Require Import @qualid
+ :name: Require Import
This loads and declares the module :n:`@qualid`
and its dependencies then imports the contents of :n:`@qualid` as described
@@ -637,10 +639,11 @@ file is a particular case of module called *library file*.
:cmd:`Import` :n:`@qualid` would.
.. cmdv:: Require Export @qualid
+ :name: Require Export
- This command acts as ``Require Import`` :n:`@qualid`,
- but if a further module, say `A`, contains a command ``Require Export`` `B`,
- then the command ``Require Import`` `A` also imports the module `B.`
+ This command acts as :cmd:`Require Import` :n:`@qualid`,
+ but if a further module, say `A`, contains a command :cmd:`Require Export` `B`,
+ then the command :cmd:`Require Import` `A` also imports the module `B.`
.. cmdv:: Require [Import | Export] {+ @qualid }
@@ -653,7 +656,7 @@ file is a particular case of module called *library file*.
.. cmdv:: From @dirpath Require @qualid
- This command acts as ``Require``, but picks
+ This command acts as :cmd:`Require`, but picks
any library whose absolute name is of the form dirpath.dirpath’.qualid
for some `dirpath’`. This is useful to ensure that the :n:`@qualid` library
comes from a given package by making explicit its absolute root.
@@ -895,6 +898,7 @@ interactively, they cannot be part of a vernacular file loaded via
necessary.
.. cmdv:: Backtrack @num @num @num
+ :name: Backtrack
.. deprecated:: 8.4
@@ -1022,12 +1026,14 @@ Controlling display
output, printing only identifiers.
.. opt:: Printing Width @num
+ :name: Printing Width
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.
.. opt:: Printing Depth @num
+ :name: Printing Depth
This option controls the nesting depth of the formatter used for pretty-
printing. Beyond this depth, display of subterms is replaced by dots. At the
@@ -1208,28 +1214,29 @@ scope of their effect. There are four kinds of commands:
+ Commands whose default is to extend their effect both outside the
section and the module or library file they occur in. For these
commands, the Local modifier limits the effect of the command to the
- current section or module it occurs in. As an example, the ``Coercion``
- (see Section :ref:`coercions`) and ``Strategy`` (see :ref:`here <vernac-strategy>`)
- commands belong to this category.
+ current section or module it occurs in. As an example, the :cmd:`Coercion`
+ and :cmd:`Strategy` commands belong to this category.
+ Commands whose default behavior is to stop their effect at the end
of the section they occur in but to extent their effect outside the module or
library file they occur in. For these commands, the Local modifier limits the
effect of the command to the current module if the command does not occur in a
section and the Global modifier extends the effect outside the current
sections and current module if the command occurs in a section. As an example,
- the :cmd:`Implicit Arguments`, :cmd:`Ltac` or :cmd:`Notation` commands belong
+ the :cmd:`Arguments`, :cmd:`Ltac` or :cmd:`Notation` commands belong
to this category. Notice that a subclass of these commands do not support
extension of their scope outside sections at all and the Global is not
applicable to them.
+ Commands whose default behavior is to stop their effect at the end
- of the section or module they occur in. For these commands, the Global
+ of the section or module they occur in. For these commands, the ``Global``
modifier extends their effect outside the sections and modules they
- occurs in. The ``Transparent`` and ``Opaque`` (see Section :ref:`vernac-controlling-the-reduction-strategies`) commands belong to this category.
+ occurs in. The :cmd:`Transparent` and :cmd:`Opaque`
+ (see Section :ref:`vernac-controlling-the-reduction-strategies`) commands
+ belong to this category.
+ Commands whose default behavior is to extend their effect outside
sections but not outside modules when they occur in a section and to
extend their effect outside the module or library file they occur in
when no section contains them.For these commands, the Local modifier
limits the effect to the current section or module while the Global
modifier extends the effect outside the module even when the command
- occurs in a section. The ``Set`` and ``Unset`` commands belong to this
+ occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this
category.
diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
index e12e4d897..682553c31 100644
--- a/doc/sphinx/user-extensions/proof-schemes.rst
+++ b/doc/sphinx/user-extensions/proof-schemes.rst
@@ -26,6 +26,7 @@ induction for objects in type `identᵢ`.
natural in case of inductively defined relations.
.. cmdv:: Scheme Equality for @ident
+ :name: Scheme Equality
Tries to generate a Boolean equality and a proof of the decidability of the usual equality. If `ident`
involves some other inductive types, their equality has to be defined first.
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 6958b5f26..3b95a37ed 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -916,9 +916,8 @@ Binding arguments of a constant to an interpretation scope
.. seealso::
- :cmd:`About @qualid`
- The command to show the scopes bound to the arguments of a
- function is described in Section 2.
+ The command :cmd:`About` can be used to show the scopes bound to the
+ arguments of a function.
.. note::