diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 7 | ||||
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 110 | ||||
| -rw-r--r-- | doc/sphinx/changes.rst | 8 | ||||
| -rwxr-xr-x | doc/sphinx/conf.py | 3 | ||||
| -rw-r--r-- | doc/sphinx/language/core/basic.rst | 26 | ||||
| -rw-r--r-- | doc/sphinx/language/core/coinductive.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/language/core/definitions.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/core/inductive.rst | 32 | ||||
| -rw-r--r-- | doc/sphinx/language/core/records.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/language/core/variants.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/canonical.rst | 34 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 88 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 49 |
14 files changed, 225 insertions, 160 deletions
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 298ea4b4ab..104f84a253 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -99,15 +99,15 @@ coercions. Enables the program mode, in which 1) typechecking allows subset coercions and 2) the elaboration of pattern matching of :cmd:`Fixpoint` and - :cmd:`Definition` act as if the :attr:`program` attribute had been + :cmd:`Definition` acts as if the :attr:`program` attribute has been used, generating obligations if there are unresolved holes after typechecking. -.. attr:: program +.. attr:: program{? = {| yes | no } } :name: program; Program - Allows using the Program mode on a specific - definition. An alternative syntax is to use the legacy ``Program`` + This :term:`boolean attribute` allows using or disabling the Program mode on a specific + definition. An alternative and commonly used syntax is to use the legacy ``Program`` prefix (cf. :n:`@legacy_attr`) as it is elsewhere in this chapter. .. _syntactic_control: diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 2474c784b8..22527dc379 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -320,10 +320,9 @@ Summary of the commands maintained. Like any command declaring a record, this command supports the - :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, - :attr:`universes(template)`, :attr:`universes(notemplate)`, - :attr:`universes(cumulative)`, :attr:`universes(noncumulative)` and - :attr:`private(matching)` attributes. + :attr:`universes(polymorphic)`, :attr:`universes(template)`, + :attr:`universes(cumulative)`, and :attr:`private(matching)` + attributes. .. cmd:: Existing Class @qualid diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 1fb337b30a..4615a8dfca 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -122,33 +122,37 @@ in a universe strictly higher than :g:`Set`. Polymorphic, Monomorphic ------------------------- -.. attr:: universes(polymorphic) - :name: universes(polymorphic); Polymorphic +.. attr:: universes(polymorphic{? = {| yes | no } }) + :name: universes(polymorphic); Polymorphic; Monomorphic + + This :term:`boolean attribute` can be used to control whether universe + polymorphism is enabled in the definition of an inductive type. + There is also a legacy syntax using the ``Polymorphic`` prefix (see + :n:`@legacy_attr`) which, as shown in the examples, is more + commonly used. + + When ``universes(polymorphic=no)`` is used, global universe constraints + are produced, even when the :flag:`Universe Polymorphism` flag is + on. There is also a legacy syntax using the ``Monomorphic`` prefix + (see :n:`@legacy_attr`). - This attribute can be used to declare universe polymorphic - definitions and inductive types. There is also a legacy syntax - using the ``Polymorphic`` prefix (see :n:`@legacy_attr`) which, as - shown in the examples, is more commonly used. +.. attr:: universes(monomorphic) -.. flag:: Universe Polymorphism + .. deprecated:: 8.13 - This flag is off by default. When it is on, new declarations are - polymorphic unless the :attr:`universes(monomorphic)` attribute is - used. + Use :attr:`universes(polymorphic=no) <universes(polymorphic)>` + instead. -.. attr:: universes(monomorphic) - :name: universes(monomorphic); Monomorphic +.. flag:: Universe Polymorphism - This attribute can be used to declare universe monomorphic - definitions and inductive types (i.e. global universe constraints - are produced), even when the :flag:`Universe Polymorphism` flag is - on. There is also a legacy syntax using the ``Monomorphic`` prefix - (see :n:`@legacy_attr`). + This flag is off by default. When it is on, new declarations are + polymorphic unless the :attr:`universes(polymorphic=no) <universes(polymorphic)>` + attribute is used to override the default. Many other commands can be used to declare universe polymorphic or monomorphic constants depending on whether the :flag:`Universe -Polymorphism` flag is on or the :attr:`universes(polymorphic)` or -:attr:`universes(monomorphic)` attributes are used: +Polymorphism` flag is on or the :attr:`universes(polymorphic)` +attribute is used: - :cmd:`Lemma`, :cmd:`Axiom`, etc. can be used to declare universe polymorphic constants. @@ -171,19 +175,27 @@ Polymorphism` flag is on or the :attr:`universes(polymorphic)` or Cumulative, NonCumulative ------------------------- -.. attr:: universes(cumulative) - :name: universes(cumulative); Cumulative +.. attr:: universes(cumulative{? = {| yes | no } }) + :name: universes(cumulative); Cumulative; NonCumulative Polymorphic inductive types, coinductive types, variants and - records can be declared cumulative using this attribute or the - legacy ``Cumulative`` prefix (see :n:`@legacy_attr`) which, as + records can be declared cumulative using this :term:`boolean attribute` + or the legacy ``Cumulative`` prefix (see :n:`@legacy_attr`) which, as shown in the examples, is more commonly used. This means that two instances of the same inductive type (family) are convertible based on the universe variances; they do not need to be equal. - .. exn:: The cumulative and noncumulative attributes can only be used in a polymorphic context. + When the attribtue is off, the inductive type is non-cumulative + even if the :flag:`Polymorphic Inductive Cumulativity` flag is on. + There is also a legacy syntax using the ``NonCumulative`` prefix + (see :n:`@legacy_attr`). + + This means that two instances of the same inductive type (family) + are convertible only if all the universes are equal. + + .. exn:: The cumulative attribute can only be used in a polymorphic context. Using this attribute requires being in a polymorphic context, i.e. either having the :flag:`Universe Polymorphism` flag on, or @@ -192,26 +204,21 @@ Cumulative, NonCumulative .. note:: - ``#[ universes(polymorphic), universes(cumulative) ]`` can be - abbreviated into ``#[ universes(polymorphic, cumulative) ]``. + :n:`#[ universes(polymorphic{? = yes }), universes(cumulative{? = {| yes | no } }) ]` can be + abbreviated into :n:`#[ universes(polymorphic{? = yes }, cumulative{? = {| yes | no } }) ]`. -.. flag:: Polymorphic Inductive Cumulativity +.. attr:: universes(noncumulative) - When this flag is on (it is off by default), it makes all - subsequent *polymorphic* inductive definitions cumulative, unless - the :attr:`universes(noncumulative)` attribute is used. It has no - effect on *monomorphic* inductive definitions. + .. deprecated:: 8.13 -.. attr:: universes(noncumulative) - :name: universes(noncumulative); NonCumulative + Use :attr:`universes(cumulative=no) <universes(cumulative)>` instead. - Declares the inductive type as non-cumulative even if the - :flag:`Polymorphic Inductive Cumulativity` flag is on. There is - also a legacy syntax using the ``NonCumulative`` prefix (see - :n:`@legacy_attr`). +.. flag:: Polymorphic Inductive Cumulativity - This means that two instances of the same inductive type (family) - are convertible only if all the universes are equal. + When this flag is on (it is off by default), it makes all + subsequent *polymorphic* inductive definitions cumulative, unless + the :attr:`universes(cumulative=no) <universes(cumulative)>` attribute is + used to override the default. It has no effect on *monomorphic* inductive definitions. Consider the examples below. @@ -246,6 +253,7 @@ The following is an example of a record with non-trivial subtyping relation: .. coqtop:: all Polymorphic Cumulative Record packType := {pk : Type}. + About packType. :g:`packType` binds a covariant universe, i.e. @@ -254,6 +262,27 @@ The following is an example of a record with non-trivial subtyping relation: E[Γ] ⊢ \mathsf{packType}@\{i\} =_{βδιζη} \mathsf{packType}@\{j\}~\mbox{ whenever }~i ≤ j +Specifying cumulativity +~~~~~~~~~~~~~~~~~~~~~~~ + +The variance of the universe parameters for a cumulative inductive may be specified by the user. + +For the following type, universe ``a`` has its variance automatically +inferred (it is irrelevant), ``b`` is required to be irrelevant, +``c`` is covariant and ``d`` is invariant. With these annotations +``c`` and ``d`` have less general variances than would be inferred. + +.. coqtop:: all + + Polymorphic Cumulative Inductive Dummy@{a *b +c =d} : Prop := dummy. + About Dummy. + +Insufficiently restrictive variance annotations lead to errors: + +.. coqtop:: all + + Fail Polymorphic Cumulative Record bad@{*a} := {p : Type@{a}}. + An example of a proof using cumulativity ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -280,7 +309,7 @@ An example of a proof using cumulativity End down. Cumulativity Weak Constraints ------------------------------ +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. flag:: Cumulativity Weak Constraints @@ -383,6 +412,7 @@ Explicit Universes | _ | @qualid univ_decl ::= @%{ {* @ident } {? + } {? %| {*, @univ_constraint } {? + } } %} + cumul_univ_decl ::= @%{ {* {? {| = | + | * } } @ident } {? + } {? %| {*, @univ_constraint } {? + } } %} univ_constraint ::= @universe_name {| < | = | <= } @universe_name The syntax has been extended to allow users to explicitly bind names diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index de5dbe79cc..24fa71059c 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -147,7 +147,7 @@ Specification language, type inference This makes typeclasses with declared modes more robust with respect to the order of resolution. (`#10858 <https://github.com/coq/coq/pull/10858>`_, - fixes `#9058 <https://github.com/coq/coq/issues/9058>_`, by Matthieu Sozeau). + fixes `#9058 <https://github.com/coq/coq/issues/9058>`_, by Matthieu Sozeau). - **Added:** Warn when manual implicit arguments are used in unexpected positions of a term (e.g. in `Check id (forall {x}, x)`) or when an implicit @@ -533,8 +533,8 @@ Flags, options and attributes - **Removed:** Unqualified ``polymorphic``, ``monomorphic``, ``template``, ``notemplate`` attributes (they were deprecated since Coq 8.10). - Use :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, - :attr:`universes(template)` and :attr:`universes(notemplate)` instead + Use :attr:`universes(polymorphic)`, ``universes(monomorphic)``, + :attr:`universes(template)` and ``universes(notemplate)`` instead (`#11663 <https://github.com/coq/coq/pull/11663>`_, by Théo Zimmermann). - **Deprecated:** :flag:`Hide Obligations` flag @@ -545,7 +545,7 @@ Flags, options and attributes <https://github.com/coq/coq/pull/11162>`_, by Enrico Tassi). - **Added:** New attributes supported when defining an inductive type - :attr:`universes(cumulative)`, :attr:`universes(noncumulative)` and + :attr:`universes(cumulative)`, ``universes(noncumulative)`` and :attr:`private(matching)`, which correspond to legacy attributes ``Cumulative``, ``NonCumulative``, and the previously undocumented ``Private`` (`#11665 <https://github.com/coq/coq/pull/11665>`_, by diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 75ac2a76cd..af5d1e3a00 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -221,7 +221,8 @@ html_context = { 'versions': [ ("dev", "https://coq.github.io/doc/master/refman/"), ("stable", "https://coq.inria.fr/distrib/current/refman/"), - ("v8.12", "https://coq.github.io/doc/v8.12/refman/"), + ("v8.13", "https://coq.github.io/doc/v8.13/refman/"), + ("8.12", "https://coq.inria.fr/distrib/V8.12.1/refman/"), ("8.11", "https://coq.inria.fr/distrib/V8.11.2/refman/"), ("8.10", "https://coq.inria.fr/distrib/V8.10.2/refman/"), ("8.9", "https://coq.inria.fr/distrib/V8.9.1/refman/"), diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 5406da38a1..2b262b89c0 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -369,6 +369,7 @@ this attribute`. attributes ::= {* #[ {*, @attribute } ] } {* @legacy_attr } attribute ::= @ident {? @attr_value } attr_value ::= = @string + | = @ident | ( {*, @attribute } ) legacy_attr ::= {| Local | Global } | {| Polymorphic | Monomorphic } @@ -379,21 +380,22 @@ this attribute`. The order of top-level attributes doesn't affect their meaning. ``#[foo,bar]``, ``#[bar,foo]``, ``#[foo]#[bar]`` and ``#[bar]#[foo]`` are equivalent. +:gdef:`Boolean attributes <boolean attribute>` take the form :n:`@ident__attr{? = {| yes | no } }`. +When the :n:`{| yes | no }` value is omitted, the default is :n:`yes`. + The legacy attributes (:n:`@legacy_attr`) provide an older, alternate syntax for certain attributes. They are equivalent to new attributes as follows: -================ ================================ -Legacy attribute New attribute -================ ================================ -`Local` :attr:`local` -`Global` :attr:`global` -`Polymorphic` :attr:`universes(polymorphic)` -`Monomorphic` :attr:`universes(monomorphic)` -`Cumulative` :attr:`universes(cumulative)` -`NonCumulative` :attr:`universes(noncumulative)` -`Private` :attr:`private(matching)` -`Program` :attr:`program` -================ ================================ +============================= ================================ +Legacy attribute New attribute +============================= ================================ +`Local` :attr:`local` +`Global` :attr:`global` +`Polymorphic`, `Monomorphic` :attr:`universes(polymorphic)` +`Cumulative`, `NonCumulative` :attr:`universes(cumulative)` +`Private` :attr:`private(matching)` +`Program` :attr:`program` +============================= ================================ Attributes appear in the HTML documentation in blue or gray boxes after the label "Attribute". In the pdf, they appear after the diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst index 3e2ecdc0f0..43bbc8b40d 100644 --- a/doc/sphinx/language/core/coinductive.rst +++ b/doc/sphinx/language/core/coinductive.rst @@ -26,10 +26,8 @@ More information on co-inductive definitions can be found in For co-inductive types, the only elimination principle is case analysis. This command supports the :attr:`universes(polymorphic)`, - :attr:`universes(monomorphic)`, :attr:`universes(template)`, - :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, - :attr:`universes(noncumulative)`, :attr:`private(matching)` - and :attr:`using` attributes. + :attr:`universes(template)`, :attr:`universes(cumulative)`, + :attr:`private(matching)`, and :attr:`using` attributes. .. example:: diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index 79489c85f6..57771c9036 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -90,7 +90,7 @@ Section :ref:`typing-rules`. computation on :n:`@term`. These commands also support the :attr:`universes(polymorphic)`, - :attr:`universes(monomorphic)`, :attr:`program` (see :ref:`program_definition`), + :attr:`program` (see :ref:`program_definition`), :attr:`canonical` and :attr:`using` attributes. If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index d3bd787587..251b5e4955 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -8,13 +8,14 @@ Inductive types .. cmd:: Inductive @inductive_definition {* with @inductive_definition } - .. insertprodn inductive_definition constructor + .. insertprodn inductive_definition cumul_ident_decl .. prodn:: - inductive_definition ::= {? > } @ident_decl {* @binder } {? %| {* @binder } } {? : @type } {? := {? @constructors_or_record } } {? @decl_notations } + inductive_definition ::= {? > } @cumul_ident_decl {* @binder } {? %| {* @binder } } {? : @type } {? := {? @constructors_or_record } } {? @decl_notations } constructors_or_record ::= {? %| } {+| @constructor } | {? @ident } %{ {*; @record_field } {? ; } %} constructor ::= @ident {* @binder } {? @of_type } + cumul_ident_decl ::= @ident {? @cumul_univ_decl } This command defines one or more inductive types and its constructors. Coq generates destructors @@ -31,10 +32,8 @@ Inductive types proposition). This command supports the :attr:`universes(polymorphic)`, - :attr:`universes(monomorphic)`, :attr:`universes(template)`, - :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, - :attr:`universes(noncumulative)` and :attr:`private(matching)` - attributes. + :attr:`universes(template)`, :attr:`universes(cumulative)`, and + :attr:`private(matching)` attributes. Mutually inductive types can be defined by including multiple :n:`@inductive_definition`\s. The :n:`@ident`\s are simultaneously added to the environment before the types of constructors are checked. @@ -1057,7 +1056,7 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or at level :math:`\Type` (without annotations or hiding it behind a definition) template polymorphic if possible. - This can be prevented using the :attr:`universes(notemplate)` + This can be prevented using the :attr:`universes(template=no) <universes(template)>` attribute. Template polymorphism and full universe polymorphism (see Chapter @@ -1076,11 +1075,12 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or the :attr:`universes(template)` attribute: in this case, the warning is not emitted. -.. attr:: universes(template) +.. attr:: universes(template{? = {| yes | no } }) + :name: universes(template) - This attribute can be used to explicitly declare an inductive type - as template polymorphic, whether the :flag:`Auto Template - Polymorphism` flag is on or off. + This :term:`boolean attribute` can be used to explicitly declare an + inductive type as template polymorphic, whether the :flag:`Auto + Template Polymorphism` flag is on or off. .. exn:: template and polymorphism not compatible @@ -1093,11 +1093,15 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or The attribute was used but the inductive definition does not satisfy the criterion to be template polymorphic. + When ``universes(template=no)`` is used, it will prevent an + inductive type to be template polymorphic, even if the :flag:`Auto + Template Polymorphism` flag is on. + .. attr:: universes(notemplate) - This attribute can be used to prevent an inductive type to be - template polymorphic, even if the :flag:`Auto Template - Polymorphism` flag is on. + .. deprecated:: 8.13 + + Use :attr:`universes(template=no) <universes(template)>` instead. In practice, the rule **Ind-Family** is used by Coq only when all the inductive types of the inductive definition are declared with an arity diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst index e6df3ee9f5..7eedbcd59a 100644 --- a/doc/sphinx/language/core/records.rst +++ b/doc/sphinx/language/core/records.rst @@ -53,10 +53,8 @@ expressions. In this sense, the :cmd:`Record` construction allows defining :cmd:`Record` and :cmd:`Structure` are synonyms. This command supports the :attr:`universes(polymorphic)`, - :attr:`universes(monomorphic)`, :attr:`universes(template)`, - :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, - :attr:`universes(noncumulative)` and :attr:`private(matching)` - attributes. + :attr:`universes(template)`, :attr:`universes(cumulative)`, and + :attr:`private(matching)` attributes. More generally, a record may have explicitly defined (a.k.a. manifest) fields. For instance, we might have: diff --git a/doc/sphinx/language/core/variants.rst b/doc/sphinx/language/core/variants.rst index 645986be9c..6ac6626dbe 100644 --- a/doc/sphinx/language/core/variants.rst +++ b/doc/sphinx/language/core/variants.rst @@ -17,10 +17,8 @@ Variants this variant, unless the :flag:`Nonrecursive Elimination Schemes` flag is on. This command supports the :attr:`universes(polymorphic)`, - :attr:`universes(monomorphic)`, :attr:`universes(template)`, - :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, - :attr:`universes(noncumulative)` and :attr:`private(matching)` - attributes. + :attr:`universes(template)`, :attr:`universes(cumulative)`, and + :attr:`private(matching)` attributes. .. exn:: The @natural th argument of @ident must be @ident in @type. :undocumented: diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst index 48120503af..f7ce7f1c6c 100644 --- a/doc/sphinx/language/extensions/canonical.rst +++ b/doc/sphinx/language/extensions/canonical.rst @@ -87,29 +87,27 @@ in :ref:`canonicalstructures`; here only a simple example is given. If a same field occurs in several canonical structures, then only the structure declared first as canonical is considered. - .. attr:: canonical(false) +.. attr:: canonical{? = {| yes | no } } + :name: canonical - To prevent a field from being involved in the inference of - canonical instances, its declaration can be annotated with the - :attr:`canonical(false)` attribute (cf. the syntax of - :n:`@record_field`). + This boolean attribute can decorate a :cmd:`Definition` or + :cmd:`Let` command. It is equivalent to having a :cmd:`Canonical + Structure` declaration just after the command. - .. example:: + To prevent a field from being involved in the inference of + canonical instances, its declaration can be annotated with + ``canonical=no`` (cf. the syntax of :n:`@record_field`). - For instance, when declaring the :g:`Setoid` structure above, the - :g:`Prf_equiv` field declaration could be written as follows. - - .. coqdoc:: + .. example:: - #[canonical(false)] Prf_equiv : equivalence Carrier Equal + For instance, when declaring the :g:`Setoid` structure above, the + :g:`Prf_equiv` field declaration could be written as follows. - See :ref:`canonicalstructures` for a more realistic example. + .. coqdoc:: -.. attr:: canonical + #[canonical=no] Prf_equiv : equivalence Carrier Equal - This attribute can decorate a :cmd:`Definition` or :cmd:`Let` command. - It is equivalent to having a :cmd:`Canonical Structure` declaration just - after the command. + See :ref:`hierarchy_of_structures` for a more realistic example. .. cmd:: Print Canonical Projections {* @reference } @@ -248,6 +246,8 @@ for each component of the pair. The declaration associates to the key ``*`` relation ``pair_eq`` whenever the type constructor ``*`` is applied to two types being themselves in the ``EQ`` class. +.. _hierarchy_of_structures: + Hierarchy of structures ---------------------------- @@ -331,7 +331,7 @@ We need to define a new class that inherits from both ``EQ`` and ``LE``. LE_class : LE.class T; extra : mixin (EQ.Pack T EQ_class) (LE.cmp T LE_class) }. - Structure type := _Pack { obj : Type; #[canonical(false)] class_of : class obj }. + Structure type := _Pack { obj : Type; #[canonical=no] class_of : class obj }. Arguments Mixin {e le} _. diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index ec3689bbbe..5d36ec3cf9 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -92,14 +92,54 @@ CoqMakefile is a makefile for ``GNU Make`` with targets to build the project (e.g. generate .vo or .html files from .v or compile .ml* files) and install it in the ``user-contrib`` directory where the Coq - library is installed. Run ``make`` with the ``-f CoqMakefile`` - option to use ``CoqMakefile``. + library is installed. CoqMakefile.conf contains make variables assignments that reflect the contents of the ``_CoqProject`` file as well as the path relevant to Coq. +The recommended approach is to invoke ``CoqMakefile`` from a standard +``Makefile`` of the following form: + +.. example:: + + :: + + # KNOWNTARGETS will not be passed along to CoqMakefile + KNOWNTARGETS := CoqMakefile extra-stuff extra-stuff2 + # KNOWNFILES will not get implicit targets from the final rule, and so + # depending on them won't invoke the submake + # Warning: These files get declared as PHONY, so any targets depending + # on them always get rebuilt + KNOWNFILES := Makefile _CoqProject + + .DEFAULT_GOAL := invoke-coqmakefile + + CoqMakefile: Makefile _CoqProject + $(COQBIN)coq_makefile -f _CoqProject -o CoqMakefile + + invoke-coqmakefile: CoqMakefile + $(MAKE) --no-print-directory -f CoqMakefile $(filter-out $(KNOWNTARGETS),$(MAKECMDGOALS)) + + .PHONY: invoke-coqmakefile $(KNOWNFILES) + + #################################################################### + ## Your targets here ## + #################################################################### + + # This should be the last rule, to handle any targets not declared above + %: invoke-coqmakefile + @true + +The advantage of a wrapper, compared to directly calling the generated +``Makefile``, is that it +provides a target independent of the version of Coq to regenerate a +``Makefile`` specific to the current version of Coq. Additionally, the +master ``Makefile`` can be extended with targets not specific to Coq. +Including the generated makefile with an include directive is +discouraged, since the contents of this file, including variable names and +status of rules, may change in the future. An optional file ``CoqMakefile.local`` can be provided by the user in order to extend ``CoqMakefile``. In particular one can declare custom actions to be @@ -453,50 +493,6 @@ line timing data: This target requires python to build the table. -Reusing/extending the generated Makefile -++++++++++++++++++++++++++++++++++++++++ - -Including the generated makefile with an include directive is -discouraged. The contents of this file, including variable names and -status of rules shall change in the future. Users are advised to -include ``Makefile.conf`` or call a target of the generated Makefile as in -``make -f Makefile target`` from another Makefile. - -One way to get access to all targets of the generated ``CoqMakefile`` is to -have a generic target for invoking unknown targets. - -.. example:: - - :: - - # KNOWNTARGETS will not be passed along to CoqMakefile - KNOWNTARGETS := CoqMakefile extra-stuff extra-stuff2 - # KNOWNFILES will not get implicit targets from the final rule, and so - # depending on them won't invoke the submake - # Warning: These files get declared as PHONY, so any targets depending - # on them always get rebuilt - KNOWNFILES := Makefile _CoqProject - - .DEFAULT_GOAL := invoke-coqmakefile - - CoqMakefile: Makefile _CoqProject - $(COQBIN)coq_makefile -f _CoqProject -o CoqMakefile - - invoke-coqmakefile: CoqMakefile - $(MAKE) --no-print-directory -f CoqMakefile $(filter-out $(KNOWNTARGETS),$(MAKECMDGOALS)) - - .PHONY: invoke-coqmakefile $(KNOWNFILES) - - #################################################################### - ## Your targets here ## - #################################################################### - - # This should be the last rule, to handle any targets not declared above - %: invoke-coqmakefile - @true - - - Building a subset of the targets with ``-j`` ++++++++++++++++++++++++++++++++++++++++++++ diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index f36767b207..16c8586a9f 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -214,7 +214,7 @@ have to be observed for notations starting with a symbol, e.g., rules starting with “\ ``{``\ ” or “\ ``(``\ ” should be put at level 0. The list of Coq predefined notations can be found in the chapter on :ref:`thecoqlibrary`. -Displaying symbolic notations +Use of notations for printing ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The command :cmd:`Notation` has an effect both on the Coq parser and on the @@ -323,6 +323,26 @@ at the time of use of the notation. scope. Obviously, expressions printed by means of such extra printing rules will not be reparsed to the same form. +.. note:: + + When several notations can be used to print a given term, the + notations which capture the largest subterm of the term are used + preferentially. Here is an example: + + .. coqtop:: in + + Notation "x < y" := (lt x y) (at level 70). + Notation "x < y < z" := (lt x y /\ lt y z) (at level 70, y at next level). + + Check (0 < 1 /\ 1 < 2). + + When several notations match the same subterm, or incomparable + subterms of the term to print, the notation declared most recently + is selected. Moreover, reimporting a library or module declares the + notations of this library or module again. If the notation is in a + scope (see :ref:`Scopes`), either the scope has to be opened or a + delimiter has to exist in the scope for the notation to be usable. + The Infix command ~~~~~~~~~~~~~~~~~~ @@ -787,20 +807,39 @@ nested iterating pattern, the second placeholder is finally filled with the terminating expression. In the example above, the iterator :math:`φ([~]_E , [~]_I)` is :math:`cons [~]_E\, [~]_I` -and the terminating expression is ``nil``. Here are other examples: +and the terminating expression is ``nil``. + +Here is another example with the pattern associating on the left: .. coqtop:: in Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) (at level 0). +Here is an example with more involved recursive patterns: + +.. coqtop:: in + Notation "[| t * ( x , y , .. , z ) ; ( a , b , .. , c ) * u |]" := (pair (pair .. (pair (pair t x) (pair t y)) .. (pair t z)) (pair .. (pair (pair a u) (pair b u)) .. (pair c u))) (t at level 39). -Notations with recursive patterns can be reserved like standard -notations, they can also be declared within -:ref:`notation scopes <Scopes>`. +To give a flavor of the extent and limits of the mechanism, here is an +example showing a notation for a chain of equalities. It relies on an +artificial expansion of the intended denotation so as to expose a +``φ(x, .. φ(y,t) ..)`` structure, with the drawback that if ever the +beta-redexes are contracted, the notations stops to be used for +printing. + +.. coqtop:: in + + Notation "x ⪯ y ⪯ .. ⪯ z ⪯ t" := + ((fun b A a => a <= b /\ A b) y .. ((fun b A a => a <= b /\ A b) z (fun b => b <= t)) .. x) + (at level 70, y at next level, z at next level, t at next level). + +Note finally that notations with recursive patterns can be reserved like +standard notations, they can also be declared within :ref:`notation +scopes <Scopes>`. .. _RecursiveNotationsWithBinders: |