diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-04-14 21:57:53 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-04-14 21:59:15 +0200 |
| commit | ab2e6772c6cbe2e6fa8851a1b399222a2a7740e3 (patch) | |
| tree | 8bd8a4bd811af8a57f7b675741221a5a9c849511 | |
| parent | 3cc6a433d025996ea4a61969517d45ffbc9fd8a9 (diff) | |
[Sphinx] Fix all remaining warnings.
24 files changed, 352 insertions, 323 deletions
diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index 64d4eddf0..1d3b66173 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -305,6 +305,8 @@ explicitations (as for terms 2.7.11). end). +.. _matching-dependent: + Matching objects of dependent types ----------------------------------- @@ -414,6 +416,7 @@ length, by writing I have a copy of :g:`b` in type :g:`listn 0` resp :g:`listn (S n')`. +.. _match-in-patterns: Patterns in ``in`` ~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index 0e72c996f..d60387f4f 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -707,20 +707,18 @@ instances are tried at each node of the search tree). To speed it up, declare your constant as rigid for proof search using the command ``Typeclasses Opaque`` (see :ref:`TypeclassesTransparent`). - Strategies for rewriting ------------------------ - Definitions ~~~~~~~~~~~ -The generalized rewriting tactic is based on a set of strategies that -can be combined to obtain custom rewriting procedures. Its set of -strategies is based on Elan’s rewriting strategies :ref:`TODO-102-biblio`. Rewriting +The generalized rewriting tactic is based on a set of strategies that can be +combined to obtain custom rewriting procedures. Its set of strategies is based +on Elan’s rewriting strategies :cite:`Luttik97specificationof`. Rewriting strategies are applied using the tactic ``rewrite_strat s`` where ``s`` is a -strategy expression. Strategies are defined inductively as described -by the following grammar: +strategy expression. Strategies are defined inductively as described by the +following grammar: .. productionlist:: rewriting s, t, u : `strategy` diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index 68e071d7c..ec1b942e0 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -272,25 +272,24 @@ Activating the Printing of Coercions Classes as Records ------------------ -We allow the definition of *Structures with Inheritance* (or -classes as records) by extending the existing ``Record`` macro -(see Section :ref:`record-types`). Its new syntax is: - -.. cmd:: Record {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } }. - - The first identifier `ident` is the name of the defined record and - `sort` is its type. The optional identifier after ``:=`` is the name - of the constuctor (it will be ``Build_``\ `ident` if not given). - The other identifiers are the names of the fields, and the `term` - are their respective types. If ``:>`` is used instead of ``:`` in - the declaration of a field, then the name of this field is automatically - declared as a coercion from the record name to the class of this - field type. Remark that the fields always verify the uniform - inheritance condition. If the optional ``>`` is given before the - record name, then the constructor name is automatically declared as - a coercion from the class of the last field type to the record name - (this may fail if the uniform inheritance condition is not - satisfied). +We allow the definition of *Structures with Inheritance* (or classes as records) +by extending the existing :cmd:`Record` macro. Its new syntax is: + +.. cmdv:: Record {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } }. + + The first identifier `ident` is the name of the defined record and + `sort` is its type. The optional identifier after ``:=`` is the name + of the constuctor (it will be ``Build_``\ `ident` if not given). + The other identifiers are the names of the fields, and the `term` + are their respective types. If ``:>`` is used instead of ``:`` in + the declaration of a field, then the name of this field is automatically + declared as a coercion from the record name to the class of this + field type. Remark that the fields always verify the uniform + inheritance condition. If the optional ``>`` is given before the + record name, then the constructor name is automatically declared as + a coercion from the class of the last field type to the record name + (this may fail if the uniform inheritance condition is not + satisfied). .. note:: diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index a2940881d..1c3fdeb43 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -135,8 +135,7 @@ support types, avoiding uses of proof-irrelevance that would come up when reasoning with equality on the subset types themselves. The next two commands are similar to their standard counterparts -Definition (see Section :ref:`gallina_def`) and Fixpoint -(see Section :ref:`TODO-1.3.4-Fixpoint`) +:cmd:`Definition` and :cmd:`Fixpoint` in that they define constants. However, they may require the user to prove some goals to construct the final definitions. @@ -197,7 +196,7 @@ The optional order annotation follows the grammar: + :g:`wf R x` which is equivalent to :g:`measure x (R)`. The structural fixpoint operator behaves just like the one of |Coq| (see -Section :ref:`TODO-1.3.4-Fixpoint`), except it may also generate obligations. It works +:cmd:`Fixpoint`), except it may also generate obligations. It works with mutually recursive definitions too. .. coqtop:: reset none diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index b861892cb..ae666a0d4 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -701,7 +701,7 @@ for |Coq|’s type-checker. Let us see why: At each step of rewriting, the whole context is duplicated in the proof term. Then, a tactic that does hundreds of rewriting generates huge proof terms. Since ``ACDSimpl`` was too slow, Samuel Boutin rewrote -it using reflection (see his article in TACS’97 [Bou97]_). Later, it +it using reflection (see :cite:`Bou97`). Later, it was rewritten by Patrick Loiseleur: the new tactic does not any more require ``ACDSimpl`` to compile and it makes use of |bdi|-reduction not only to replace the rewriting steps, but also to achieve the diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index add03b946..8861cac8a 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -148,11 +148,10 @@ database. Sections and contexts --------------------- -To ease the parametrization of developments by type classes, we -provide a new way to introduce variables into section contexts, -compatible with the implicit argument mechanism. The new command works -similarly to the ``Variables`` vernacular (:ref:`TODO-1.3.2-Definitions`), except it -accepts any binding context as argument. For example: +To ease the parametrization of developments by type classes, we provide a new +way to introduce variables into section contexts, compatible with the implicit +argument mechanism. The new command works similarly to the :cmd:`Variables` +vernacular, except it accepts any binding context as argument. For example: .. coqtop:: all diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib index 247f32103..ef50923c7 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -675,7 +675,6 @@ s}, author = {G. Huet}, booktitle = {A perspective in Theoretical Computer Science. Commemorative Volume for Gift Siromoney}, editor = {R. Narasimhan}, - note = {Also in~\cite{CoC89}}, publisher = {World Scientific Publishing}, title = {{The Constructive Engine}}, year = {1989} @@ -815,11 +814,12 @@ of the {ML} language}, } @inproceedings{Luttik97specificationof, - Author = {Sebastiaan P. Luttik and Eelco Visser}, - Booktitle = {2nd International Workshop on the Theory and Practice of Algebraic Specifications (ASF+SDF'97), Electronic Workshops in Computing}, - Publisher = {Springer-Verlag}, - Title = {Specification of Rewriting Strategies}, - Year = {1997}} + author = {Sebastiaan P. Luttik and Eelco Visser}, + booktitle = {2nd International Workshop on the Theory and Practice of Algebraic Specifications (ASF+SDF'97), Electronic Workshops in Computing}, + publisher = {Springer-Verlag}, + title = {Specification of Rewriting Strategies}, + year = {1997} +} @Book{MaL84, author = {{P. Martin-L\"of}}, diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index 67de2ae68..4a313df0c 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -60,7 +60,7 @@ continuous reading. However, it has some structure that is explained below. - The first part describes the specification language, |Gallina|. - Chapters :ref:`thegallinaspecificationlanguage` and :ref:`extensionsofgallina` describe the concrete + Chapters :ref:`gallinaspecificationlanguage` and :ref:`extensionsofgallina` describe the concrete syntax as well as the meaning of programs, theorems and proofs in the Calculus of Inductive Constructions. Chapter :ref:`thecoqlibrary` describes the standard library of |Coq|. Chapter :ref:`calculusofinductiveconstructions` is a mathematical description @@ -76,7 +76,7 @@ below. Chapter :ref:`proofhandling`. In Chapter :ref:`tactics`, all commands that realize one or more steps of the proof are presented: we call them *tactics*. The language to combine these tactics into complex proof - strategies is given in Chapter :ref:`thetacticlanguage`. Examples of tactics + strategies is given in Chapter :ref:`ltac`. Examples of tactics are described in Chapter :ref:`detailedexamplesoftactics`. - The third part describes how to extend the syntax of |Coq|. It diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 839f3ce56..5a2aa0a1f 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -401,9 +401,11 @@ can decide if two programs are *intentionally* equal (one says *convertible*). Convertibility is described in this section. -.. _β-reduction: +.. _beta-reduction: + +β-reduction +~~~~~~~~~~~ -**β-reduction.** We want to be able to identify some terms as we can identify the application of a function to a given argument with its result. For instance the identity function over a given type T can be written @@ -427,9 +429,11 @@ theoretically of great importance but we will not detail them here and refer the interested reader to :cite:`Coq85`. -.. _ι-reduction: +.. _iota-reduction: + +ι-reduction +~~~~~~~~~~~ -**ι-reduction.** A specific conversion rule is associated to the inductive objects in the global environment. We shall give later on (see Section :ref:`Well-formed-inductive-definitions`) the precise rules but it @@ -438,9 +442,11 @@ constructor behaves as expected. This reduction is called ι-reduction and is more precisely studied in :cite:`Moh93,Wer94`. -.. _δ-reduction: +.. _delta-reduction: + +δ-reduction +~~~~~~~~~~~ -**δ-reduction.** We may have variables defined in local contexts or constants defined in the global environment. It is legal to identify such a reference with its value, that is to expand (or unfold) it into its value. This @@ -461,9 +467,11 @@ reduction is called δ-reduction and shows as follows. E[Γ] ⊢ c~\triangleright_δ~t -.. _ζ-reduction: +.. _zeta-reduction: + +ζ-reduction +~~~~~~~~~~~ -**ζ-reduction.** |Coq| allows also to remove local definitions occurring in terms by replacing the defined variable by its value. The declaration being destroyed, this reduction differs from δ-reduction. It is called @@ -478,9 +486,11 @@ destroyed, this reduction differs from δ-reduction. It is called E[Γ] ⊢ \letin{x}{u}{t}~\triangleright_ζ~\subst{t}{x}{u} -.. _η-expansion: +.. _eta-expansion: + +η-expansion +~~~~~~~~~~~ -**η-expansion.** Another important concept is η-expansion. It is legal to identify any term :math:`t` of functional type :math:`∀ x:T, U` with its so-called η-expansion @@ -517,9 +527,11 @@ for :math:`x` an arbitrary variable name fresh in :math:`t`. convertible to the type of the original term :math:`∀ x:\Type(1),\Type(1).` -.. _Convertibility: +.. _convertibility: + +Convertibility +~~~~~~~~~~~~~~ -**Convertibility.** Let us write :math:`E[Γ] ⊢ t \triangleright u` for the contextual closure of the relation :math:`t` reduces to :math:`u` in the global environment :math:`E` and local context :math:`Γ` with one of the previous @@ -823,8 +835,9 @@ to inconsistent systems. We restrict ourselves to definitions which satisfy a syntactic criterion of positivity. Before giving the formal rules, we need a few definitions: +Arity of a given sort ++++++++++++++++++++++ -**Type is an Arity of Sort S.** A type :math:`T` is an *arity of sort s* if it converts to the sort s or to a product :math:`∀ x:T,U` with :math:`U` an arity of sort s. @@ -834,7 +847,8 @@ product :math:`∀ x:T,U` with :math:`U` an arity of sort s. :math:`\Prop`. -**Type is an Arity.** +Arity ++++++ A type :math:`T` is an *arity* if there is a :math:`s∈ \Sort` such that :math:`T` is an arity of sort s. @@ -844,32 +858,34 @@ sort s. :math:`A→ Set` and :math:`∀ A:\Prop,A→ \Prop` are arities. -**Type of Constructor of I.** +Type constructor +++++++++++++++++ We say that T is a *type of constructor of I* in one of the following two cases: - + :math:`T` is :math:`(I~t_1 … t_n )` + :math:`T` is :math:`∀ x:U,T'` where :math:`T'` is also a type of constructor of :math:`I` - - .. example:: :math:`\nat` and :math:`\nat→\nat` are types of constructor of :math:`\nat`. :math:`∀ A:Type,\List~A` and :math:`∀ A:Type,A→\List~A→\List~A` are types of constructor of :math:`\List`. -**Positivity Condition.** +.. _positivity: + +Positivity Condition +++++++++++++++++++++ + The type of constructor :math:`T` will be said to *satisfy the positivity condition* for a constant :math:`X` in the following cases: - + :math:`T=(X~t_1 … t_n )` and :math:`X` does not occur free in any :math:`t_i` + :math:`T=∀ x:U,V` and :math:`X` occurs only strictly positively in :math:`U` and the type :math:`V` satisfies the positivity condition for :math:`X`. - -**Occurs Strictly Positively.** +Strict positivity ++++++++++++++++++ + The constant :math:`X` *occurs strictly positively* in :math:`T` in the following cases: @@ -889,11 +905,12 @@ cases: any of the :math:`t_i`, and the (instantiated) types of constructor :math:`\subst{C_i}{p_j}{a_j}_{j=1… m}` of :math:`I` satisfy the nested positivity condition for :math:`X` -**Nested Positivity Condition.** +Nested Positivity ++++++++++++++++++ + The type of constructor :math:`T` of :math:`I` *satisfies the nested positivity condition* for a constant :math:`X` in the following cases: - + :math:`T=(I~b_1 … b_m~u_1 … u_p)`, :math:`I` is an inductive definition with :math:`m` parameters and :math:`X` does not occur in any :math:`u_i` + :math:`T=∀ x:U,V` and :math:`X` occurs only strictly positively in :math:`U` and the type :math:`V` @@ -940,12 +957,11 @@ For instance, if one considers the type │ ╰─ list satisfies the positivity condition for list A ... (bullet 1) - - - .. _Correctness-rules: -**Correctness rules.** +Correctness rules ++++++++++++++++++ + We shall now describe the rules allowing the introduction of a new inductive definition. @@ -1012,7 +1028,9 @@ has type :math:`\Type(k)` with :math:`k<j` and :math:`k≤ i`. .. _Template-polymorphism: -**Template polymorphism.** +Template polymorphism ++++++++++++++++++++++ + Inductive types declared in Type are polymorphic over their arguments in Type. If :math:`A` is an arity of some sort and s is a sort, we write :math:`A_{/s}` for the arity obtained from :math:`A` by replacing its sort with s. @@ -1217,9 +1235,11 @@ Coquand in :cite:`Coq92`. One is the definition by pattern-matching. The second one is a definition by guarded fixpoints. -.. _The-match…with-end-construction: +.. _match-construction: + +The match ... with ... end construction ++++++++++++++++++++++++++++++++++++++++ -**The match…with …end construction** The basic idea of this operator is that we have an object :math:`m` in an inductive type :math:`I` and we want to prove a property which possibly depends on :math:`m`. For this, it is enough to prove the property for @@ -1623,9 +1643,8 @@ Given a variable :math:`y` of type an inductive definition in a declaration ones in which one of the :math:`I_l` occurs) are structurally smaller than y. -The following definitions are correct, we enter them using the ``Fixpoint`` -command as described in Section :ref:`TODO-1.3.4` and show the internal -representation. +The following definitions are correct, we enter them using the :cmd:`Fixpoint` +command and show the internal representation. .. example:: .. coqtop:: all diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index c5da866b8..6af6e7897 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -48,6 +48,7 @@ at the |Coq| root directory; this includes the modules ``Tactics``. Module ``Logic_Type`` also makes it in the initial state. +.. _init-notations: Notations ~~~~~~~~~ @@ -929,9 +930,8 @@ tactics (see Chapter :ref:`tactics`), there are also: Goal forall x y z:R, x * y * z <> 0. intros; split_Rmult. -These tactics has been written with the tactic language Ltac -described in Chapter :ref:`thetacticlanguage`. - +These tactics has been written with the tactic language |Ltac| +described in Chapter :ref:`ltac`. List library ~~~~~~~~~~~~ diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index ce10c651a..f474eade7 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -193,9 +193,9 @@ other arguments are the parameters of the inductive type. This message is followed by an explanation of this impossibility. There may be three reasons: - #. The name `ident` already exists in the environment (see Section :ref:`TODO-1.3.1-axioms`). + #. The name `ident` already exists in the environment (see :cmd:`Axiom`). #. The body of `ident` uses an incorrect elimination for - `ident` (see Sections :ref:`TODO-1.3.4-fixpoint` and :ref:`Destructors`). + `ident` (see :cmd:`Fixpoint` and :ref:`Destructors`). #. The type of the projections `ident` depends on previous projections which themselves could not be defined. @@ -212,7 +212,7 @@ other arguments are the parameters of the inductive type. During the definition of the one-constructor inductive definition, all the errors of inductive definitions, as described in Section -:ref:`TODO-1.3.3-inductive-definitions`, may also occur. +:ref:`gallina-inductive-definitions`, may also occur. **See also** Coercions and records in Section :ref:`coercions-classes-as-records` of the chapter devoted to coercions. @@ -316,7 +316,7 @@ printed back as :g:`match` constructs. Variants and extensions of :g:`match` ------------------------------------- -.. _extended pattern-matching: +.. _mult-match: Multiple and nested pattern-matching ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -330,8 +330,9 @@ into a sequence of match on simple patterns. Especially, a construction defined using the extended match is generally printed under its expanded form (see ``Set Printing Matching`` in :ref:`controlling-match-pp`). -See also: :ref:`extended pattern-matching`. +See also: :ref:`extendedpatternmatching`. +.. _if-then-else: Pattern-matching on boolean values: the if expression ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -722,7 +723,7 @@ used by ``Function``. A more precise description is given below. the following are defined: + `ident_rect`, `ident_rec` and `ident_ind`, which reflect the pattern - matching structure of `term` (see the documentation of :ref:`TODO-1.3.3-Inductive`); + matching structure of `term` (see :cmd:`Inductive`); + The inductive `R_ident` corresponding to the graph of `ident` (silently); + `ident_complete` and `ident_correct` which are inversion information linking the function and its graph. @@ -778,7 +779,7 @@ Section mechanism The sectioning mechanism can be used to to organize a proof in structured sections. Then local declarations become available (see -Section :ref:`TODO-1.3.2-Definitions`). +Section :ref:`gallina-definitions`). .. cmd:: Section @ident. @@ -1240,10 +1241,6 @@ qualified name. 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``. -.. cmd:: Locate Module @qualid. - - Prints the full name of the module `qualid`. - Libraries and qualified names --------------------------------- @@ -1256,7 +1253,7 @@ The theories developed in |Coq| are stored in *library files* which are hierarchically classified into *libraries* and *sublibraries*. To express this hierarchy, library names are represented by qualified identifiers qualid, i.e. as list of identifiers separated by dots (see -:ref:`TODO-1.2.3-identifiers`). For instance, the library file ``Mult`` of the standard +:ref:`gallina-identifiers`). For instance, the library file ``Mult`` of the standard |Coq| library ``Arith`` is named ``Coq.Arith.Mult``. The identifier that starts the name of a library is called a *library root*. All library files of the standard library of |Coq| have the reserved root |Coq| but library @@ -1300,13 +1297,13 @@ names also applies to library file names. |Coq| maintains a table called the name table which maps partially qualified names of constructions to absolute names. This table is updated by the -commands ``Require`` (see :ref:`compiled-files`), ``Import`` and ``Export`` (see :ref:`here <import_qualid>`) and +commands :cmd:`Require`, :cmd:`Import` and :cmd:`Export` and also each time a new declaration is added to the context. An absolute name is called visible from a given short or partially qualified name when this latter name is enough to denote it. This means that the short or partially qualified name is mapped to the absolute name in |Coq| name table. Definitions flagged as Local are only accessible with -their fully qualified name (see :ref:`TODO-1.3.2-definitions`). +their fully qualified name (see :ref:`gallina-definitions`). It may happen that a visible name is hidden by the short name or a qualified name of another construction. In this case, the name that @@ -1328,8 +1325,7 @@ accessible, absolute names can never be hidden. Locate nat. -See also: Command Locate in :ref:`TODO-6.3.10-locate-qualid` and Locate Library in -:ref:`TODO-6.6.11-locate-library`. +See also: Commands :cmd:`Locate` and :cmd:`Locate Library`. .. _libraries-and-filesystem: @@ -1589,6 +1585,7 @@ Declaring Implicit Arguments To set implicit arguments *a posteriori*, one can use the command: .. cmd:: Arguments @qualid {* @possibly_bracketed_ident }. + :name: Arguments (implicits) where the list of `possibly_bracketed_ident` is a prefix of the list of arguments of `qualid` where the ones to be declared implicit are @@ -1802,6 +1799,8 @@ declares implicit arguments to be automatically inserted when a function is partially applied and the next argument of the function is an implicit one. +.. _explicit-applications: + Explicit applications ~~~~~~~~~~~~~~~~~~~~~ @@ -2147,16 +2146,17 @@ Printing universes .. opt:: Printing Universes. -Turn this option on to activate the display of the actual level of each occurrence of ``Type``. -See :ref:`Sorts` for details. This wizard option, in combination -with ``Set Printing All`` (see :ref:`printing_constructions_full`) can help to diagnose failures -to unify terms apparently identical but internally different in the -Calculus of Inductive Constructions. +Turn this option on to activate the display of the actual level of each +occurrence of :g:`Type`. See :ref:`Sorts` for details. This wizard option, in +combination with :opt:`Printing All` can help to diagnose failures to unify +terms apparently identical but internally different in the Calculus of Inductive +Constructions. The constraints on the internal level of the occurrences of Type (see :ref:`Sorts`) can be printed using the command .. cmd:: Print {? Sorted} Universes. + :name: Print Universes If the optional ``Sorted`` option is given, each universe will be made equivalent to a numbered label reflecting its level (with a linear @@ -2164,7 +2164,7 @@ ordering) in the universe hierarchy. This command also accepts an optional output filename: -.. cmd:: Print {? Sorted} Universes @string. +.. cmdv:: Print {? Sorted} Universes @string. If `string` ends in ``.dot`` or ``.gv``, the constraints are printed in the DOT language, and can be processed by Graphviz tools. The format is @@ -2227,7 +2227,7 @@ existential variable used in the same context as its context of definition is wr Existential variables can be named by the user upon creation using the syntax ``?``\ `ident`. This is useful when the existential variable needs to be explicitly handled later in the script (e.g. -with a named-goal selector, see :ref:`TODO-9.2-goal-selectors`). +with a named-goal selector, see :ref:`goal-selectors`). .. _explicit-display-existentials: @@ -2252,7 +2252,7 @@ is not specified and is implementation-dependent. The inner tactic may use any variable defined in its scope, including repeated alternations between variables introduced by term binding as well as those introduced by tactic binding. The expression `tacexpr` can be any tactic -expression as described in :ref:`thetacticlanguage`. +expression as described in :ref:`ltac`. .. coqtop:: all diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 6458ceeaa..246f45b3e 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1,4 +1,4 @@ -.. _BNF-syntax: +.. _gallinaspecificationlanguage: ------------------------------------ The Gallina specification language @@ -188,6 +188,8 @@ Coq terms are typed. Coq types are recognized by the same syntactic class as :token`term`. We denote by :token:`type` the semantic subclass of types inside the syntactic class :token:`term`. +.. _gallina-identifiers: + Qualified identifiers and simple identifiers -------------------------------------------- @@ -230,6 +232,8 @@ There are three sorts :g:`Set`, :g:`Prop` and :g:`Type`. More on sorts can be found in Section :ref:`sorts`. +.. _binders: + Binders ------- @@ -312,7 +316,7 @@ left. The notation ``(ident := term)`` for arguments is used for making explicit the value of implicit arguments (see -Section :ref:`Implicits-explicitation`). +Section :ref:`explicit-applications`). Type cast --------- @@ -330,6 +334,8 @@ Expressions often contain redundant pieces of information. Subterms that can be automatically inferred by Coq can be replaced by the symbol ``_`` and Coq will guess the missing piece of information. +.. _let-in: + Let-in definitions ------------------ @@ -350,7 +356,7 @@ expression is used to analyze the structure of an inductive objects and to apply specific treatments accordingly. This paragraph describes the basic form of pattern-matching. See -Section :ref:`Mult-match` and Chapter :ref:`Mult-match-full` for the description +Section :ref:`Mult-match` and Chapter :ref:`extendedpatternmatching` for the description of the general form. The basic form of pattern-matching is characterized by a single :token:`match_item` expression, a :token:`mult_pattern` restricted to a single :token:`pattern` and :token:`pattern` restricted to the form @@ -417,7 +423,7 @@ accepted and has the same meaning as the previous one. The second subcase is only relevant for annotated inductive types such as the equality predicate (see Section :ref:`Equality`), the order predicate on natural numbers or the type of lists of a given -length (see Section :ref:`listn`). In this configuration, the +length (see Section :ref:`matching-dependent`). In this configuration, the type of each branch can depend on the type dependencies specific to the branch and the whole pattern-matching expression has a type determined by the specific dependencies in the type of the term being matched. This @@ -460,18 +466,17 @@ in are available. There are specific notations for case analysis on types with one or two constructors: “if … then … else …” and “let (…, ” (see -Sections :ref:`if-then-else` and :ref:`Letin`). +Sections :ref:`if-then-else` and :ref:`let-in`). Recursive functions ------------------- The expression “fix :token:`ident`:math:`_1` :token:`binder`:math:`_1` : :token:`type`:math:`_1` ``:=`` :token:`term`:math:`_1` with … with -:token:`ident`:math:`_n` :token:`binder`:math:`_n` : :token:`type`:math:`_n` ``:=`` -:token:`term`:math:`_n` for :token:`ident`:math:`_i`” denotes the -:math:`i`\ component of a block of functions defined by mutual -well-founded recursion. It is the local counterpart of the ``Fixpoint`` -command. See Section :ref:`Fixpoint` for more details. When +:token:`ident`:math:`_n` :token:`binder`:math:`_n` : :token:`type`:math:`_n` +``:=`` :token:`term`:math:`_n` for :token:`ident`:math:`_i`” denotes the +:math:`i`\ component of a block of functions defined by mutual well-founded +recursion. It is the local counterpart of the :cmd:`Fixpoint` command. When :math:`n=1`, the “for :token:`ident`:math:`_i`” clause is omitted. The expression “cofix :token:`ident`:math:`_1` :token:`binder`:math:`_1` : @@ -531,6 +536,8 @@ dot. The different kinds of command are described hereafter. They all suppose that the terms occurring in the sentences are well-typed. +.. _gallina-assumptions: + Assumptions ----------- @@ -542,6 +549,8 @@ the same module. This :token:`type` is considered to be the type (or specification, or statement) assumed by :token:`ident` and we say that :token:`ident` has type :token:`type`. +.. _Axiom: + .. cmd:: Axiom @ident : @term. This command links *term* to the name *ident* as its specification in @@ -568,10 +577,9 @@ has type :token:`type`. .. cmdv:: Local Axiom @ident : @term. - Such axioms are never made accessible through their unqualified - name by ``Import`` and its variants (see :ref:`Import`). You - have to explicitly give their fully qualified name to refer to - them. + Such axioms are never made accessible through their unqualified name by + :cmd:`Import` and its variants. You have to explicitly give their fully + qualified name to refer to them. .. cmdv:: Conjecture @ident : @term @@ -580,11 +588,11 @@ has type :token:`type`. .. cmd:: Variable @ident : @term. This command links :token:`term` to the name :token:`ident` in the context of -the current section (see Section :ref:`Section` for a description of the section -mechanism). When the current section is closed, name :token:`ident` will be -unknown and every object using this variable will be explicitly parametrized -(the variable is *discharged*). Using the ``Variable`` command out of any -section is equivalent to using ``Local Parameter``. +the current section (see Section :ref:`section-mechanism` for a description of +the section mechanism). When the current section is closed, name :token:`ident` +will be unknown and every object using this variable will be explicitly +parametrized (the variable is *discharged*). Using the ``Variable`` command out +of any section is equivalent to using ``Local Parameter``. .. exn:: @ident already exists @@ -609,7 +617,7 @@ logical postulates (i.e. when the assertion *term* is of sort ``Prop``), and to use the keywords ``Parameter`` and ``Variable`` in other cases (corresponding to the declaration of an abstract mathematical entity). -.. _gallina_def: +.. _gallina-definitions: Definitions ----------- @@ -620,7 +628,7 @@ way to abbreviate a term. In any case, the name can later be replaced at any time by its definition. The operation of unfolding a name into its definition is called -:math:`\delta`-conversion (see Section :ref:`delta`). A +:math:`\delta`-conversion (see Section :ref:`delta-reduction`). A definition is accepted by the system if and only if the defined term is well-typed in the current context of the definition and if the name is not already used. The name defined by the definition is called a @@ -628,7 +636,7 @@ not already used. The name defined by the definition is called a type which is the type of its body. A formal presentation of constants and environments is given in -Section :ref:`Typed-terms`. +Section :ref:`typing-rules`. .. cmd:: Definition @ident := @term. @@ -654,7 +662,7 @@ Section :ref:`Typed-terms`. .. cmdv:: Local Definition @ident := @term. Such definitions are never made accessible through their - unqualified name by Import and its variants (see :ref:`Import`). + unqualified name by :cmd:`Import` and its variants. You have to explicitly give their fully qualified name to refer to them. .. cmdv:: Example @ident := @term. @@ -667,7 +675,7 @@ These are synonyms of the Definition forms. .. exn:: The term @term has type @type while it is expected to have type @type -See also Sections :ref:`Opaque,Transparent,unfold`. +See also :cmd:`Opaque`, :cmd:`Transparent`, :tac:`unfold`. .. cmd:: Let @ident := @term. @@ -687,7 +695,10 @@ prefixed by the let-in definition ``let`` :token:`ident` ``:=`` :token:`term` .. cmdv:: Let CoFixpoint @ident @cofix_body {* with @cofix_body}. -See also Sections :ref:`Section,Opaque,Transparent,unfold`. +See also Sections :ref:`section-mechanism`, commands :cmd:`Opaque`, +:cmd:`Transparent`, and tactic :tacn:`unfold`. + +.. _gallina-inductive-definitions: Inductive definitions --------------------- @@ -707,7 +718,7 @@ The name :token:`ident` is the name of the inductively defined type and :token:`sort` is the universes where it lives. The :token:`ident` are the names of its constructors and :token:`type` their respective types. The types of the constructors have to satisfy a *positivity condition* (see Section -:ref:`Positivity`) for :token:`ident`. This condition ensures the soundness of +:ref:`positivity`) for :token:`ident`. This condition ensures the soundness of the inductive definition. If this is the case, the :token:`ident` are added to the environment with their respective types. Accordingly to the universe where the inductive type lives (e.g. its type :token:`sort`), Coq provides a number of @@ -848,8 +859,7 @@ arguments of the constructors rather than their full type. The ``Variant`` keyword is identical to the ``Inductive`` keyword, except that it disallows recursive definition of types (in particular lists cannot be defined with the Variant keyword). No induction scheme is generated for -this variant, unless the option ``Nonrecursive Elimination Schemes`` is set -(see :ref:`set-nonrecursive-elimination-schemes`). +this variant, unless :opt:`Nonrecursive Elimination Schemes` is set. .. exn:: The @num th argument of @ident must be @ident in @type @@ -891,7 +901,8 @@ instead of parameters but it will sometimes give a different (bigger) sort for the inductive definition and will produce a less convenient rule for case elimination. -See also Sections :ref:`Cic-inductive-definitions,Tac-induction`. +See also Section :ref:`inductive-definitions` and the :tacn:`induction` +tactic. Mutually defined inductive types ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -960,7 +971,9 @@ section is closed, the variables declared in the section and occurring free in the declaration are added as parameters to the inductive definition. -See also Section :ref:`Section`. +See also Section :ref:`section-mechanism`. + +.. _coinductive-types: Co-inductive types ~~~~~~~~~~~~~~~~~~ @@ -982,12 +995,12 @@ Coq using the ``CoInductive`` command: CoInductive Stream : Set := Seq : nat -> Stream -> Stream. -The syntax of this command is the same as the command ``Inductive`` (see -Section :ref:`gal-Inductive-Definitions`. Notice that no principle of induction -is derived from the definition of a co-inductive type, since such principles -only make sense for inductive ones. For co-inductive ones, the only elimination -principle is case analysis. For example, the usual destructors on streams -:g:`hd:Stream->nat` and :g:`tl:Str->Str` can be defined as follows: +The syntax of this command is the same as the command :cmd:`Inductive`. Notice +that no principle of induction is derived from the definition of a co-inductive +type, since such principles only make sense for inductive ones. For co-inductive +ones, the only elimination principle is case analysis. For example, the usual +destructors on streams :g:`hd:Stream->nat` and :g:`tl:Str->Str` can be defined +as follows: .. coqtop:: all @@ -1007,7 +1020,7 @@ predicate is the extensional equality on streams: In order to prove the extensionally equality of two streams :g:`s1` and :g:`s2` we have to construct an infinite proof of equality, that is, an infinite object of type :g:`(EqSt s1 s2)`. We will see how to introduce infinite objects in -Section :ref:`CoFixpoint`. +Section :ref:`cofixpoint`. Definition of recursive functions --------------------------------- @@ -1016,12 +1029,14 @@ Definition of functions by recursion over inductive objects ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ This section describes the primitive form of definition by recursion over -inductive objects. See Section :ref:`Function` for more advanced constructions. -The command: +inductive objects. See the :cmd:`Function` command for more advanced +constructions. + +.. _Fixpoint: .. cmd:: Fixpoint @ident @params {struct @ident} : @type := @term. -allows defining functions by pattern-matching over inductive objects +This command allows defining functions by pattern-matching over inductive objects using a fixed point construction. The meaning of this declaration is to define :token:`ident` a recursive function with arguments specified by the binders in :token:`params` such that :token:`ident` applied to arguments corresponding @@ -1063,7 +1078,8 @@ respective values to be returned, as functions of the parameters of the corresponding constructor. Thus here when :g:`n` equals :g:`O` we return :g:`m`, and when :g:`n` equals :g:`(S p)` we return :g:`(S (add p m))`. -The match operator is formally described in detail in Section :ref:`Caseexpr`. +The match operator is formally described in detail in Section +:ref:`match-construction`. The system recognizes that in the inductive call :g:`(add p m)` the first argument actually decreases because it is a *pattern variable* coming from :g:`match n with`. @@ -1151,7 +1167,10 @@ The size of trees and forests can be defined the following way: end. A generic command Scheme is useful to build automatically various mutual -induction principles. It is described in Section :ref:`Scheme`. +induction principles. It is described in Section +:ref:`proofschemes-induction-principles`. + +.. _cofixpoint: Definitions of recursive objects in co-inductive types ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1160,8 +1179,8 @@ Definitions of recursive objects in co-inductive types introduces a method for constructing an infinite object of a coinductive type. For example, the stream containing all natural numbers can be -introduced applying the following method to the number :ref:`O` (see -Section :ref:`CoInductiveTypes` for the definition of :g:`Stream`, :g:`hd` and +introduced applying the following method to the number :g:`O` (see +Section :ref:`coinductive-types` for the definition of :g:`Stream`, :g:`hd` and :g:`tl`): .. coqtop:: all @@ -1204,8 +1223,8 @@ the normal forms of a term: .. cmdv:: CoFixpoint @ident : @type := @term {+ with @ident : @type := @term } - As in the ``Fixpoint`` command (see Section :ref:`Fixpoint`), it is possible - to introduce a block of mutually dependent methods. + As in the :cmd:`Fixpoint` command, it is possible to introduce a block of + mutually dependent methods. .. _Assertions: @@ -1214,7 +1233,7 @@ Assertions and proofs An assertion states a proposition (or a type) of which the proof (or an inhabitant of the type) is interactively built using tactics. The interactive -proof mode is described in Chapter :ref:`Proof-handling` and the tactics in +proof mode is described in Chapter :ref:`proofhandling` and the tactics in Chapter :ref:`Tactics`. The basic assertion command is: .. cmd:: Theorem @ident : @type. @@ -1245,15 +1264,14 @@ the theorem is bound to the name :token:`ident` in the environment. .. cmdv:: Theorem @ident : @type {* with @ident : @type}. - This command is useful for theorems that are proved by simultaneous - induction over a mutually inductive assumption, or that assert - mutually dependent statements in some mutual co-inductive type. It is - equivalent to ``Fixpoint`` or ``CoFixpoint`` (see - Section :ref:`CoFixpoint`) but using tactics to build - the proof of the statements (or the body of the specification, - depending on the point of view). The inductive or co-inductive types - on which the induction or coinduction has to be done is assumed to be - non ambiguous and is guessed by the system. + This command is useful for theorems that are proved by simultaneous induction + over a mutually inductive assumption, or that assert mutually dependent + statements in some mutual co-inductive type. It is equivalent to + :cmd:`Fixpoint` or :cmd:`CoFixpoint` but using tactics to build the proof of + the statements (or the body of the specification, depending on the point of + view). The inductive or co-inductive types on which the induction or + coinduction has to be done is assumed to be non ambiguous and is guessed by + the system. Like in a ``Fixpoint`` or ``CoFixpoint`` definition, the induction hypotheses have to be used on *structurally smaller* arguments (for a ``Fixpoint``) or @@ -1261,7 +1279,7 @@ the theorem is bound to the name :token:`ident` in the environment. recursive proof arguments are correct is done only at the time of registering the lemma in the environment. To know if the use of induction hypotheses is correct at some time of the interactive development of a proof, use the - command Guarded (see Section :ref:`Guarded`). + command :cmd:`Guarded`. The command can be used also with ``Lemma``, ``Remark``, etc. instead of ``Theorem``. @@ -1270,12 +1288,12 @@ the theorem is bound to the name :token:`ident` in the environment. This allows defining a term of type :token:`type` using the proof editing mode. It behaves as Theorem but is intended to be used in conjunction with - Defined (see :ref:`Defined`) in order to define a constant of which the - computational behavior is relevant. + :cmd:`Defined` in order to define a constant of which the computational + behavior is relevant. - The command can be used also with ``Example`` instead of ``Definition``. + The command can be used also with :cmd:`Example` instead of :cmd:`Definition`. - See also Sections :ref:`Opaque` :ref:`Transparent` :ref:`unfold`. + See also :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`. .. cmdv:: Let @ident : @type. @@ -1301,7 +1319,7 @@ A proof starts by the keyword Proof. Then Coq enters the proof editing mode until the proof is completed. The proof editing mode essentially contains tactics that are described in chapter :ref:`Tactics`. Besides tactics, there are commands to manage the proof editing mode. They are described in Chapter -:ref:`Proof-handling`. When the proof is completed it should be validated and +:ref:`proofhandling`. When the proof is completed it should be validated and put in the environment using the keyword Qed. .. exn:: @ident already exists @@ -1319,7 +1337,7 @@ put in the environment using the keyword Qed. side, Qed (or Defined, see below) is mandatory to validate a proof. #. Proofs ended by Qed are declared opaque. Their content cannot be - unfolded (see :ref:`Conversion-tactics`), thus + unfolded (see :ref:`performingcomputations`), thus realizing some form of *proof-irrelevance*. To be able to unfold a proof, the proof should be ended by Defined (see below). @@ -1328,7 +1346,7 @@ put in the environment using the keyword Qed. Same as ``Proof. … Qed.`` but the proof is then declared transparent, which means that its content can be explicitly used for type-checking and that it can be unfolded in conversion tactics - (see :ref:`Conversion-tactics,Opaque,Transparent`). + (see :ref:`performingcomputations`, :cmd:`Opaque`, :cmd:`Transparent`). .. cmdv:: Proof. … Admitted. diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 9f485f496..93dcfca4b 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -106,7 +106,7 @@ and ``coqtop``, unless stated otherwise: recursively available from |Coq| using absolute names (extending the dirpath prefix) (see Section :ref:`qualified-names`).Note that only those subdirectories and files which obey the lexical conventions of what is - an ident (see Section :ref:`TODO-1.1`) are taken into account. Conversely, the + an :n:`@ident` are taken into account. Conversely, the underlying file systems or operating systems may be more restrictive than |Coq|. While Linux’s ext4 file system supports any |Coq| recursive layout (within the limit of 255 bytes per file name), the default on diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index 3d144b1d6..f9903e610 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -150,8 +150,6 @@ arguments. Queries ------------ -.. _coqide_queryselected: - .. image:: ../_static/coqide-queries.png :alt: |CoqIDE| queries @@ -161,7 +159,7 @@ writing them in scripts, |CoqIDE| offers a *query pane*. The query pane can be displayed on demand by using the ``View`` menu, or using the shortcut ``F1``. Queries can also be performed by selecting a particular phrase, then choosing an item from the ``Queries`` menu. The response then appears in the message window. -Figure :ref:`fig:queryselected` shows the result after selecting of the phrase +The image above shows the result after selecting of the phrase ``Nat.mul`` in the script window, and choosing ``Print`` from the ``Queries`` menu. diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 48d58c473..59867988a 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -114,9 +114,7 @@ distinct plugins because of a clash in their auxiliary module names. .. _coqmakefilelocal: CoqMakefile.local -+++++++++++++++++ - - +~~~~~~~~~~~~~~~~~ The optional file ``CoqMakefile.local`` is included by the generated file ``CoqMakefile``. It can contain two kinds of directives. @@ -190,7 +188,7 @@ The following makefile rules can be extended. target. Timing targets and performance testing -++++++++++++++++++++++++++++++++++++++ +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The generated ``Makefile`` supports the generation of two kinds of timing data: per-file build-times, and per-line times for an individual file. @@ -365,7 +363,7 @@ line timing data: Reusing/extending the generated Makefile -++++++++++++++++++++++++++++++++++++++++ +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Including the generated makefile with an include directive is discouraged. The contents of this file, including variable names and @@ -408,8 +406,8 @@ have a generic target for invoking unknown targets. -Building a subset of the targets with -j -++++++++++++++++++++++++++++++++++++++++ +Building a subset of the targets with ``-j`` +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ To build, say, two targets foo.vo and bar.vo in parallel one can use ``make only TGTS="foo.vo bar.vo" -j``. @@ -540,27 +538,28 @@ Initially, the pretty-printing table contains the following mapping: `->` → `<-` ← `*` × `<=` ≤ `>=` ≥ `=>` ⇒ `<>` ≠ `<->` ↔ `|-` ⊢ -`\/` ∨ `/\` ∧ `~` ¬ +`\/` ∨ `/\\` ∧ `~` ¬ ==== === ==== ===== === ==== ==== === Any of these can be overwritten or suppressed using the printing commands. -.. note :: - The recognition of tokens is done by a (``ocaml``) lex - automaton and thus applies the longest-match rule. For instance, `->~` - is recognized as a single token, where |Coq| sees two tokens. It is the - responsibility of the user to insert space between tokens *or* to give - pretty-printing rules for the possible combinations, e.g. +.. note:: - :: + The recognition of tokens is done by a (``ocaml``) lex + automaton and thus applies the longest-match rule. For instance, `->~` + is recognized as a single token, where |Coq| sees two tokens. It is the + responsibility of the user to insert space between tokens *or* to give + pretty-printing rules for the possible combinations, e.g. + + :: (** printing ->~ %\ensuremath{\rightarrow\lnot}% *) -Sections. -+++++++++ +Sections +++++++++ Sections are introduced by 1 to 4 leading stars (i.e. at the beginning of the line) followed by a space. One star is a section, two stars a @@ -569,7 +568,7 @@ line. .. example:: - :: + :: (** * Well-founded relations @@ -805,9 +804,10 @@ Command line options directory ``coqdir`` (similarly to |Coq| option ``-R``). .. note:: - option ``-R`` only has - effect on the files *following* it on the command line, so you will - probably need to put this option first. + + option ``-R`` only has + effect on the files *following* it on the command line, so you will + probably need to put this option first. **Title options** @@ -821,6 +821,7 @@ Command line options beginning of each file is checked for a comment of the form: :: + (** * ModuleName : text *) where ``ModuleName`` must be the name of the file. If it is present, the diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst index fda20bff3..84810ddba 100644 --- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst +++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst @@ -736,7 +736,7 @@ and this length is decremented for each rotation down to, but not including, 1 because for a list of length ``n``, we can make exactly ``n−1`` rotations to generate at most ``n`` distinct lists. Here, it must be noticed that we use the natural numbers of Coq for the -rotation counter. On Figure :ref:`TODO-9.1-tactic-language`, we can +rotation counter. In :ref:`ltac-syntax`, we can see that it is possible to use usual natural numbers but they are only used as arguments for primitive tactics and they cannot be handled, in particular, we cannot make computations with them. So, a natural @@ -833,7 +833,7 @@ The pattern matching on goals allows a complete and so a powerful backtracking when returning tactic values. An interesting application is the problem of deciding intuitionistic propositional logic. Considering the contraction-free sequent calculi LJT* of Roy Dyckhoff -:ref:`TODO-56-biblio`, it is quite natural to code such a tactic +:cite:`Dyc92`, it is quite natural to code such a tactic using the tactic language as shown on figures: :ref:`Deciding intuitionistic propositions (1) <decidingintuitionistic1>` and :ref:`Deciding intuitionistic propositions (2) @@ -871,7 +871,7 @@ Deciding type isomorphisms A more tricky problem is to decide equalities between types and modulo isomorphisms. Here, we choose to use the isomorphisms of the simply typed λ-calculus with Cartesian product and unit type (see, for -example, :cite:`TODO-45`). The axioms of this λ-calculus are given below. +example, :cite:`RC95`). The axioms of this λ-calculus are given below. .. coqtop:: in reset diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 003d4b243..247d5d899 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -13,33 +13,34 @@ especially about its foundations, you can refer to :cite:`Del00`. Chapter :ref:`detailedexamplesoftactics` is devoted to giving examples of use of this language on small but also with non-trivial problems. +.. _ltac-syntax: + Syntax ------ -The syntax of the tactic language is given Figures :ref:`ltac, ltac_aux`. See -Chapter :ref:`gallina` for a description of the BNF metasyntax used in these -grammar rules. Various already defined entries will be used in this chapter: -entries :token:`natural`, :token:`integer`, :token:`ident`, :token:`qualid`, -:token:`term`, :token:`cpattern` and :token:`atomic_tactic` represent -respectively the natural and integer numbers, the authorized identificators and -qualified names, Coq terms and patterns and all the atomic tactics described in -Chapter :ref:`tactics`. The syntax of :token:`cpattern` is the same as that of -terms, but it is extended with pattern matching metavariables. In -:token:`cpattern`, a pattern-matching metavariable is represented with the -syntax :g:`?id` where :g:`id` is an :token:`ident`. The notation :g:`_` can also -be used to denote metavariable whose instance is irrelevant. In the notation -:g:`?id`, the identifier allows us to keep instantiations and to make -constraints whereas :g:`_` shows that we are not interested in what will be -matched. On the right hand side of pattern-matching clauses, the named -metavariable are used without the question mark prefix. There is also a special -notation for second-order pattern-matching problems: in an applicative pattern -of the form :g:`@?id id1 … idn`, the variable id matches any complex expression -with (possible) dependencies in the variables :g:`id1 … idn` and returns a -functional term of the form :g:`fun id1 … idn => term`. +The syntax of the tactic language is given below. See Chapter +:ref:`gallinaspecificationlanguage` for a description of the BNF metasyntax used +in these grammar rules. Various already defined entries will be used in this +chapter: entries :token:`natural`, :token:`integer`, :token:`ident`, +:token:`qualid`, :token:`term`, :token:`cpattern` and :token:`atomic_tactic` +represent respectively the natural and integer numbers, the authorized +identificators and qualified names, Coq terms and patterns and all the atomic +tactics described in Chapter :ref:`tactics`. The syntax of :token:`cpattern` is +the same as that of terms, but it is extended with pattern matching +metavariables. In :token:`cpattern`, a pattern-matching metavariable is +represented with the syntax :g:`?id` where :g:`id` is an :token:`ident`. The +notation :g:`_` can also be used to denote metavariable whose instance is +irrelevant. In the notation :g:`?id`, the identifier allows us to keep +instantiations and to make constraints whereas :g:`_` shows that we are not +interested in what will be matched. On the right hand side of pattern-matching +clauses, the named metavariable are used without the question mark prefix. There +is also a special notation for second-order pattern-matching problems: in an +applicative pattern of the form :g:`@?id id1 … idn`, the variable id matches any +complex expression with (possible) dependencies in the variables :g:`id1 … idn` +and returns a functional term of the form :g:`fun id1 … idn => term`. The main entry of the grammar is :n:`@expr`. This language is used in proof -mode but it can also be used in toplevel definitions as shown in -Figure :ref:`ltactop`. +mode but it can also be used in toplevel definitions as shown below. .. note:: @@ -153,6 +154,8 @@ Figure :ref:`ltactop`. ltac_def : `ident` [`ident` ... `ident`] := `expr` : | `qualid` [`ident` ... `ident`] ::= `expr` +.. _ltac-semantics: + Semantics --------- @@ -228,6 +231,8 @@ following form: independently. All the above variants work in this form too. Formally, :n:`@expr ; [ ... ]` is equivalent to :n:`[> @expr ; [> ... ] .. ]`. +.. _goal-selectors: + Goal selectors ~~~~~~~~~~~~~~ @@ -247,7 +252,7 @@ focused goals with: .. tacv:: [@ident] : @expr In this variant, :n:`@expr` is applied locally to a goal previously named - by the user (see :ref:`ExistentialVariables`). + by the user (see :ref:`existential-variables`). .. tacv:: @num : @expr @@ -275,6 +280,9 @@ focused goals with: the toplevel of a tactic expression. .. exn:: No such goal + :name: No such goal (goal selector) + + .. TODO change error message index entry For loop ~~~~~~~~ @@ -759,7 +767,7 @@ We can carry out pattern matching on terms with: matching subterm is tried. If no further subterm matches, the next clause is tried. Matching subterms are considered top-bottom and from left to right (with respect to the raw printing obtained by setting option - ``Printing All``, see Section :ref:`SetPrintingAll`). + :opt:`Printing All`). .. example:: @@ -775,6 +783,8 @@ We can carry out pattern matching on terms with: Goal True. f (3+4). +.. _ltac-match-goal: + Pattern matching on goals ~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1009,6 +1019,7 @@ Proving a subgoal as a separate lemma don’t play well with asynchronous proofs. .. exn:: Proof is not complete + :name: Proof is not complete (abstract) Tactic toplevel definitions --------------------------- @@ -1253,4 +1264,4 @@ Run-time optimization tactic This tactic behaves like :n:`idtac`, except that running it compacts the heap in the OCaml run-time system. It is analogous to the Vernacular -command ``Optimize Heap`` (see :ref:`vernac-optimizeheap`). +command :cmd:`Optimize Heap`. diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index c28e85171..a77b127eb 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -20,20 +20,18 @@ prove. Initially, the list consists only in the theorem itself. After having applied some tactics, the list of goals contains the subgoals generated by the tactics. -To each subgoal is associated a number of hypotheses called the *local -context* of the goal. Initially, the local context contains the local -variables and hypotheses of the current section (see Section :ref:`TODO_gallina_assumptions`) -and the local variables and hypotheses of the theorem statement. It is -enriched by the use of certain tactics (see e.g. ``intro`` in Section -:ref:`managingthelocalcontext`). +To each subgoal is associated a number of hypotheses called the *local context* +of the goal. Initially, the local context contains the local variables and +hypotheses of the current section (see Section :ref:`gallina-assumptions`) and +the local variables and hypotheses of the theorem statement. It is enriched by +the use of certain tactics (see e.g. :tacn:`intro`). When a proof is completed, the message ``Proof completed`` is displayed. One can then register this proof as a defined constant in the environment. Because there exists a correspondence between proofs and -terms of λ-calculus, known as the *Curry-Howard isomorphism* [[How80]_, -[Bar81]_, [Gir89]_, [Hue88]_ ], |Coq| -stores proofs as terms of |Cic|. Those terms -are called *proof terms*. +terms of λ-calculus, known as the *Curry-Howard isomorphism* +:cite:`How80,Bar81,Gir89,Hue88`, |Coq| stores proofs as terms of |Cic|. Those +terms are called *proof terms*. .. exn:: No focused proof @@ -46,13 +44,10 @@ out of the proof editing mode. Switching on/off the proof editing mode ------------------------------------------- -The proof editing mode is entered by asserting a statement, which -typically is the assertion of a theorem: - -.. cmd:: Theorem @ident [@binders] : @form. - -The list of assertion commands is given in Section :ref:TODO-assertions_and_proof`. The -command ``Goal`` can also be used. +The proof editing mode is entered by asserting a statement, which typically is +the assertion of a theorem using an assertion command like :cmd:`Theorem`. The +list of assertion commands is given in Section :ref:`Assertions`. The command +:cmd:`Goal` can also be used. .. cmd:: Goal @form. @@ -95,14 +90,13 @@ Forces the name of the original goal to be :n:`@ident`. This command (and the following ones) can only be used if the original goal has been opened using the ``Goal`` command. - .. cmd:: Admitted. This command is available in interactive editing proof mode to give up the current proof and declare the initial goal as an axiom. - .. cmd:: Proof @term. + :name: Proof `term` This command applies in proof editing mode. It is equivalent to @@ -127,7 +121,7 @@ See also: ``Proof with tactic.`` in Section .. cmd:: Proof using @ident1 ... @identn. This command applies in proof editing mode. It declares the set of -section variables (see :ref:`TODO-gallina-assumptions`) used by the proof. At ``Qed`` time, the +section variables (see :ref:`gallina-assumptions`) used by the proof. At ``Qed`` time, the system will assert that the set of section variables actually used in the proof is a subset of the declared one. @@ -354,10 +348,10 @@ Error messages: You are trying to use ``}`` but the current subproof has not been fully solved. .. exn:: No such goal + :name: No such goal (focusing) .. exn:: Brackets only support the single numbered goal selector - See also error messages about bullets below. .. _bullets: @@ -597,4 +591,4 @@ the ongoing proof. This command forces the |OCaml| runtime to perform a heap compaction. This is in general an expensive operation. See: `OCaml Gc <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_ -There is also an analogous tactic ``optimize_heap`` (see~:ref:`tactic-optimizeheap`) +There is also an analogous tactic :tac:`optimize_heap`. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index df5b36297..074c6f1e2 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -5185,6 +5185,7 @@ equivalences are indeed taken into account, otherwise only single |SSR| proposes an extension of the Search command. Its syntax is: .. cmd:: Search {? @pattern } {* {? - } %( @string %| @pattern %) {? % @ident} } {? in {+ {? - } @qualid } } + :name: Search (ssreflect) where :token:`qualid` is the name of an open module. This command returns the list of lemmas: diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 046efa730..08aa7110d 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -34,7 +34,7 @@ satisfied. If it is not the case, the tactic raises an error message. Tactics are built from atomic tactics and tactic expressions (which extends the folklore notion of tactical) to combine those atomic tactics. This chapter is devoted to atomic tactics. The tactic -language will be described in Chapter :ref:`TODO-9-Thetacticlanguage`. +language will be described in Chapter :ref:`ltac`. .. _invocation-of-tactics: @@ -42,7 +42,7 @@ Invocation of tactics ------------------------- A tactic is applied as an ordinary command. It may be preceded by a -goal selector (see Section :ref:`TODO-9.2-Semantics`). If no selector is +goal selector (see Section :ref:`ltac-semantics`). If no selector is specified, the default selector is used. .. _tactic_invocation_grammar: @@ -95,7 +95,7 @@ bindings_list`` where ``bindings_list`` may be of two different forms: + A bindings list can also be a simple list of terms :n:`{* term}`. In that case the references to which these terms correspond are determined by the tactic. In case of ``induction``, ``destruct``, ``elim`` - and ``case`` (see :ref:`TODO-9-Thetacticlanguage`) the terms have to + and ``case`` (see :ref:`ltac`) the terms have to provide instances for all the dependent products in the type of term while in the case of ``apply``, or of ``constructor`` and its variants, only instances for the dependent products that are not bound in the conclusion of the type @@ -279,7 +279,7 @@ gets the form :g:`(fun x => Q) u`:sub:`1` :g:`...` :g:`u`:sub:`n`. The apply tactic failed to match the conclusion of term and the current goal. You can help the apply tactic by transforming your goal with the -:ref:`change <change_term>` or :tacn:`pattern` tactics. +:tacn:`change` or :tacn:`pattern` tactics. .. exn:: Unable to find an instance for the variables {+ @ident}. @@ -287,7 +287,7 @@ This occurs when some instantiations of the premises of term are not deducible from the unification. This is the case, for instance, when you want to apply a transitivity property. In this case, you have to use one of the variants below: -.. cmd:: apply @term with {+ @term} +.. tacv:: apply @term with {+ @term} Provides apply with explicit instantiations for all dependent premises of the type of term that do not occur in the conclusion and consequently cannot be @@ -1091,7 +1091,7 @@ Controlling the proof flow .. tacv:: assert form - This behaves as :n:`assert (@ident : form ) but :n:`@ident` is generated by + This behaves as :n:`assert (@ident : form)` but :n:`@ident` is generated by Coq. .. tacv:: assert form by tactic @@ -1100,6 +1100,7 @@ Controlling the proof flow generated by assert. .. exn:: Proof is not complete + :name: Proof is not complete (assert) .. tacv:: assert form as intro_pattern @@ -1750,7 +1751,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) results equivalent to ``inversion`` or ``dependent inversion`` if the hypothesis is dependent. -See also :ref:`dependentinduction` for a larger example of ``dependent induction`` +See also the larger example of :tacn:`dependent induction` and an explanation of the underlying technique. .. tacn:: function induction (@qualid {+ @term}) @@ -2910,7 +2911,7 @@ the conversion in hypotheses :n:`{+ @ident}`. This tactic applies to any goal. The argument qualid must denote a defined transparent constant or local definition (see - :ref:`TODO-1.3.2-Definitions` and :ref:`vernac-controlling-the-reduction-strategies`). The tactic + :ref:`gallina-definitions` and :ref:`vernac-controlling-the-reduction-strategies`). The tactic ``unfold`` applies the :math:`\delta` rule to each occurrence of the constant to which :n:`@qualid` refers in the current goal and then replaces it with its :math:`\beta`:math:`\iota`-normal form. @@ -3608,40 +3609,37 @@ Setting implicit automation tactics In this case the tactic command typed by the user is equivalent to ``tactic``:sub:`1` ``;tactic``. -See also: ``Proof.`` in :ref:`proof-editing-mode`. + See also: ``Proof.`` in :ref:`proof-editing-mode`. -**Variants:** - -.. cmd:: Proof with tactic using {+ @ident} - Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode` + .. cmdv:: Proof with tactic using {+ @ident} -.. cmd:: Proof using {+ @ident} with tactic + Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode` - Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode` + .. cmdv:: Proof using {+ @ident} with tactic -.. cmd:: Declare Implicit Tactic tactic + Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode` - This command declares a tactic to be used to solve implicit arguments - that Coq does not know how to solve by unification. It is used every - time the term argument of a tactic has one of its holes not fully - resolved. + .. cmd:: Declare Implicit Tactic tactic -Here is an example: + This command declares a tactic to be used to solve implicit arguments + that Coq does not know how to solve by unification. It is used every + time the term argument of a tactic has one of its holes not fully + resolved. -.. example:: + .. example:: - .. coqtop:: all + .. coqtop:: all - Parameter quo : nat -> forall n:nat, n<>0 -> nat. - Notation "x // y" := (quo x y _) (at level 40). - Declare Implicit Tactic assumption. - Goal forall n m, m<>0 -> { q:nat & { r | q * m + r = n } }. - intros. - exists (n // m). + Parameter quo : nat -> forall n:nat, n<>0 -> nat. + Notation "x // y" := (quo x y _) (at level 40). + Declare Implicit Tactic assumption. + Goal forall n m, m<>0 -> { q:nat & { r | q * m + r = n } }. + intros. + exists (n // m). - The tactic ``exists (n // m)`` did not fail. The hole was solved - by ``assumption`` so that it behaved as ``exists (quo n m H)``. + The tactic ``exists (n // m)`` did not fail. The hole was solved + by ``assumption`` so that it behaved as ``exists (quo n m H)``. .. _decisionprocedures: @@ -3719,7 +3717,7 @@ and then uses :tacn:`auto` which completes the proof. Originally due to César Muñoz, these tactics (:tacn:`tauto` and :tacn:`intuition`) have been completely re-engineered by David Delahaye using -mainly the tactic language (see :ref:`TODO-9-thetacticlanguage`). The code is +mainly the tactic language (see :ref:`ltac`). The code is now much shorter and a significant increase in performance has been noticed. The general behavior with respect to dependent types, unfolding and introductions has slightly changed to get clearer semantics. This may lead to @@ -4346,7 +4344,7 @@ close the section (see also :ref:`section-mechanism`) where it was defined. If you want that a tactic macro defined in a module is usable in the modules that require it, you should put it outside of any section. -:ref:`TODO-9-Thetacticlanguage` gives examples of more complex +:ref:`ltac` gives examples of more complex user-defined tactics. .. [1] Actually, only the second subgoal will be generated since the diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index f7693d551..da4034fb8 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1393,16 +1393,15 @@ scope of their effect. There are four kinds of commands: (see Section :ref:`coercions`) and ``Strategy`` (see :ref:`here <vernac-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 ``Implicit Arguments`` (see - Section :ref:`implicitarguments`), Ltac (see Chapter :ref:`TODO-9-tactic-language`) or ``Notation`` (see Section - :ref:`notations`) 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. + 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 + 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 modifier extends their effect outside the sections and modules they diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index 1f1167c59..8a24a382a 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -108,11 +108,10 @@ induction principles when defining a new inductive type with the ``Unset Elimination Schemes`` command. It may be reactivated at any time with ``Set Elimination Schemes``. -The types declared with the keywords ``Variant`` (see :ref:`TODO-1.3.3`) and ``Record`` -(see :ref:`Record Types <record-types>`) do not have an automatic declaration of the induction -principles. It can be activated with the command -``Set Nonrecursive Elimination Schemes``. It can be deactivated again with -``Unset Nonrecursive Elimination Schemes``. +.. opt:: Nonrecursive Elimination Schemes + +This option controls whether types declared with the keywords :cmd:`Variant` and +:cmd:`Record` get an automatic declaration of the induction principles. In addition, the ``Case Analysis Schemes`` flag governs the generation of case analysis lemmas for inductive types, i.e. corresponding to the diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 0da9f2300..9965d5002 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -345,13 +345,13 @@ inductive type or a recursive constant and a notation for it. Simultaneous definition of terms and notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Thanks to reserved notations, the inductive, co-inductive, record, recursive -and corecursive definitions can benefit of customized notations. To do -this, insert a ``where`` notation clause after the definition of the -(co)inductive type or (co)recursive term (or after the definition of -each of them in case of mutual definitions). The exact syntax is given -on Figure 12.1 for inductive, co-inductive, recursive and corecursive -definitions and on Figure :ref:`record-syntax` for records. Here are examples: +Thanks to reserved notations, the inductive, co-inductive, record, recursive and +corecursive definitions can benefit of customized notations. To do this, insert +a ``where`` notation clause after the definition of the (co)inductive type or +(co)recursive term (or after the definition of each of them in case of mutual +definitions). The exact syntax is given by :token:`decl_notation` for inductive, +co-inductive, recursive and corecursive definitions and in :ref:`record-types` +for records. Here are examples: .. coqtop:: in @@ -386,20 +386,16 @@ Displaying informations about notations Locating notations ~~~~~~~~~~~~~~~~~~ -.. cmd:: Locate @symbol +To know to which notations a given symbol belongs to, use the :cmd:`Locate` +command. You can call it on any (composite) symbol surrounded by double quotes. +To locate a particular notation, use a string where the variables of the +notation are replaced by “_” and where possible single quotes inserted around +identifiers or tokens starting with a single quote are dropped. - To know to which notations a given symbol belongs to, use the command - ``Locate symbol``, where symbol is any (composite) symbol surrounded by double - quotes. To locate a particular notation, use a string where the variables of the - notation are replaced by “_” and where possible single quotes inserted around - identifiers or tokens starting with a single quote are dropped. - - .. coqtop:: all - - Locate "exists". - Locate "exists _ .. _ , _". +.. coqtop:: all - .. todo:: See also: Section 6.3.10. + Locate "exists". + Locate "exists _ .. _ , _". Notations and binders ~~~~~~~~~~~~~~~~~~~~~ @@ -437,8 +433,7 @@ Binders bound in the notation and parsed as patterns In the same way as patterns can be used as binders, as in :g:`fun '(x,y) => x+y` or :g:`fun '(existT _ x _) => x`, notations can be -defined so that any pattern (in the sense of the entry :n:`@pattern` of -Figure :ref:`term-syntax-aux`) can be used in place of the +defined so that any :n:`@pattern` can be used in place of the binder. Here is an example: .. coqtop:: in reset @@ -477,7 +472,7 @@ variable. Here is an example showing the difference: The default level for a ``pattern`` is 0. One can use a different level by using ``pattern at level`` :math:`n` where the scale is the same as the one for -terms (Figure :ref:`init-notations`). +terms (see :ref:`init-notations`). Binders bound in the notation and parsed as terms +++++++++++++++++++++++++++++++++++++++++++++++++ @@ -863,6 +858,7 @@ Binding arguments of a constant to an interpretation scope +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ .. cmd:: Arguments @qualid {+ @name%@scope} + :name: Arguments (scopes) It is possible to set in advance that some arguments of a given constant have to be interpreted in a given scope. The command is diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 663ab9d37..f09ed4b55 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -108,7 +108,7 @@ class CoqObject(ObjectDescription): annotation = self.annotation + ' ' signode += addnodes.desc_annotation(annotation, annotation) self._render_signature(signature, signode) - return self._name_from_signature(signature) + return self.options.get("name") or self._name_from_signature(signature) @property def _index_suffix(self): @@ -145,14 +145,6 @@ class CoqObject(ObjectDescription): index_text = name + self._index_suffix self.indexnode['entries'].append(('single', index_text, target, '', None)) - def run(self): - """Small extension of the parent's run method, handling user-provided names.""" - [idx, node] = super().run() - custom_name = self.options.get("name") - if custom_name: - self.add_target_and_index(custom_name, "", node.children[0]) - return [idx, node] - def add_target_and_index(self, name, _, signode): """Create a target and an index entry for name""" if name: @@ -194,13 +186,18 @@ class VernacObject(NotationObject): annotation = "Command" def _name_from_signature(self, signature): - return stringify_with_ellipses(signature) + m = re.match(r"[a-zA-Z ]+", signature) + if m: + return m.group(0).strip() class VernacVariantObject(VernacObject): """An object to represent variants of Coq commands""" index_suffix = "(cmdv)" annotation = "Variant" + def _name_from_signature(self, signature): + return None + class TacticNotationObject(NotationObject): """An object to represent Coq tactic notations""" subdomain = "tacn" |