diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index 577e4ef8e199c..3b893a7d24969 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -240,8 +240,8 @@ declaration, this constructor is declared as a coercion. Same as :cmd:`Identity Coercion` but locally to the current section. - .. cmdv:: SubClass @ident := @type - :name: SubClassVar + .. cmd:: "SubClass" @ident_decl @def_body + :name: SubClass If :n:`@type` is a class :n:`@ident'` applied to some arguments then :n:`@ident` is defined and an identity coercion of name @@ -251,7 +251,7 @@ declaration, this constructor is declared as a coercion. :n:`Definition @ident := @type.` :n:`Identity Coercion Id_@ident_@ident' : @ident >-> @ident'`. - .. cmdv:: Local SubClass @ident := @type + .. cmdv:: Local SubClass @ident_decl @def_body Same as before but locally to the current section. diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 551a0fbb50c53..8a049a2df84dc 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -840,7 +840,6 @@ Sections create local contexts which can be shared across multiple definitions. .. cmdv:: Variables {+ ( {+ @ident } : @type) } Hypothesis {+ ( {+ @ident } : @type) } Hypotheses {+ ( {+ @ident } : @type) } - :name: VariablesVar; HypothesisVar; HypothesesVar These variants are synonyms of :n:`Variable {+ ( {+ @ident } : @type) }`. diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 5cf220674967c..e784077aac570 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -49,11 +49,11 @@ Blanks Comments Comments are enclosed between ``(*`` and ``*)``. They can be nested. - They can contain any character. However, embedded :token:`string` literals must be + They can contain any character. However, embedded :n:`@string` literals must be correctly closed. Comments are treated as blanks. Identifiers - Identifiers, written :token:`ident`, are sequences of letters, digits, ``_`` and + Identifiers, written :n:`@ident`, are sequences of letters, digits, ``_`` and ``'``, that do not start with a digit or ``'``. That is, they are recognized by the following grammar (except that the string ``_`` is reserved; it is not a valid identifier): @@ -74,8 +74,8 @@ Identifiers Numerals Numerals are sequences of digits with an optional fractional part - and exponent, optionally preceded by a minus sign. :token:`int` is an integer; - a numeral without fractional or exponent parts. :token:`num` is a non-negative + and exponent, optionally preceded by a minus sign. :n:`@int` is an integer; + a numeral without fractional or exponent parts. :n:`@num` is a non-negative integer. Underscores embedded in the digits are ignored, for example ``1_000_000`` is the same as ``1000000``. @@ -179,8 +179,8 @@ Types ----- Coq terms are typed. Coq types are recognized by the same syntactic -class as :token:`term`. We denote by :production:`type` the semantic subclass -of types inside the syntactic class :token:`term`. +class as :n:`@term`. We denote by :production:`type` the semantic subclass +of types inside the syntactic class :n:`@term`. .. _gallina-identifiers: @@ -193,14 +193,14 @@ Qualified identifiers and simple identifiers qualid ::= @ident {* @field_ident } field_ident ::= .@ident -*Qualified identifiers* (:token:`qualid`) denote *global constants* +*Qualified identifiers* (:n:`@qualid`) denote *global constants* (definitions, lemmas, theorems, remarks or facts), *global variables* (parameters or axioms), *inductive types* or *constructors of inductive -types*. *Simple identifiers* (or shortly :token:`ident`) are a syntactic subset +types*. *Simple identifiers* (or shortly :n:`@ident`) are a syntactic subset of qualified identifiers. Identifiers may also denote *local variables*, while qualified identifiers do not. -Field identifiers, written :token:`field_ident`, are identifiers prefixed by +Field identifiers, written :n:`@field_ident`, are identifiers prefixed by `.` (dot) with no blank between the dot and the identifier. @@ -215,7 +215,7 @@ numbers (see :ref:`datatypes`). .. note:: - Negative integers are not at the same level as :token:`num`, for this + Negative integers are not at the same level as :n:`@num`, for this would make precedence unnatural. .. index:: @@ -257,13 +257,13 @@ There are four sorts :g:`SProp`, :g:`Prop`, :g:`Set` and :g:`Type`. propositions* (also called *strict propositions*). - :g:`Prop` is the universe of *logical propositions*. The logical propositions - themselves are typing the proofs. We denote propositions by :token:`form`. - This constitutes a semantic subclass of the syntactic class :token:`term`. + themselves are typing the proofs. We denote propositions by :n:`@form`. + This constitutes a semantic subclass of the syntactic class :n:`@term`. - :g:`Set` is the universe of *program types* or *specifications*. The specifications themselves are typing the programs. We denote - specifications by :token:`specif`. This constitutes a semantic subclass of - the syntactic class :token:`term`. + specifications by :n:`@specif`. This constitutes a semantic subclass of + the syntactic class :n:`@term`. - :g:`Type` is the type of sorts. @@ -305,14 +305,14 @@ a notation for a sequence of binding variables sharing the same type: binder can also be any pattern prefixed by a quote, e.g. :g:`'(x,y)`. Some constructions allow the binding of a variable to value. This is -called a “let-binder”. The entry :token:`binder` of the grammar accepts +called a “let-binder”. The entry :n:`@binder` of the grammar accepts either an assumption binder as defined above or a let-binder. The notation in the latter case is :n:`(@ident := @term)`. In a let-binder, only one variable can be introduced at the same time. It is also possible to give the type of the variable as follows: :n:`(@ident : @type := @term)`. -Lists of :token:`binder`\s are allowed. In the case of :g:`fun` and :g:`forall`, +Lists of :n:`@binder`\s are allowed. In the case of :g:`fun` and :g:`forall`, it is intended that at least one binder of the list is an assumption otherwise fun and forall gets identical. Moreover, parentheses can be omitted in the case of a single sequence of bindings sharing the same type (e.g.: @@ -324,9 +324,9 @@ Abstractions: fun ----------------- The expression :n:`fun @ident : @type => @term` defines the -*abstraction* of the variable :token:`ident`, of type :token:`type`, over the term -:token:`term`. It denotes a function of the variable :token:`ident` that evaluates to -the expression :token:`term` (e.g. :g:`fun x : A => x` denotes the identity +*abstraction* of the variable :n:`@ident`, of type :n:`@type`, over the term +:n:`@term`. It denotes a function of the variable :n:`@ident` that evaluates to +the expression :n:`@term` (e.g. :g:`fun x : A => x` denotes the identity function on type :g:`A`). The keyword :g:`fun` can be followed by several binders as given in Section :ref:`binders`. Functions over several variables are equivalent to an iteration of one-variable @@ -343,12 +343,12 @@ Products: forall ---------------- The expression :n:`forall @ident : @type, @term` denotes the -*product* of the variable :token:`ident` of type :token:`type`, over the term :token:`term`. +*product* of the variable :n:`@ident` of type :n:`@type`, over the term :n:`@term`. As for abstractions, :g:`forall` is followed by a binder list, and products over several variables are equivalent to an iteration of one-variable -products. Note that :token:`term` is intended to be a type. +products. Note that :n:`@term` is intended to be a type. -If the variable :token:`ident` occurs in :token:`term`, the product is called +If the variable :n:`@ident` occurs in :n:`@term`, the product is called *dependent product*. The intention behind a dependent product :g:`forall x : A, B` is twofold. It denotes either the universal quantification of the variable :g:`x` of type :g:`A` @@ -393,13 +393,13 @@ Type cast | @term10 :> The expression :n:`@term : @type` is a type cast expression. It enforces -the type of :token:`term` to be :token:`type`. +the type of :n:`@term` to be :n:`@type`. :n:`@term <: @type` locally sets up the virtual machine for checking that -:token:`term` has type :token:`type`. +:n:`@term` has type :n:`@type`. -:n:`@term <<: @type` uses native compilation for checking that :token:`term` -has type :token:`type`. +:n:`@term <<: @type` uses native compilation for checking that :n:`@term` +has type :n:`@type`. .. index:: _ @@ -427,8 +427,8 @@ Let-in definitions | let ' @pattern in @pattern := @term return @term100 in @term :n:`let @ident := @term in @term’` -denotes the local binding of :token:`term` to the variable -:token:`ident` in :token:`term`’. There is a syntactic sugar for let-in +denotes the local binding of :n:`@term` to the variable +:n:`@ident` in :n:`@term`’. There is a syntactic sugar for let-in definition of functions: :n:`let @ident {+ @binder} := @term in @term’` stands for :n:`let @ident := fun {+ @binder} => @term in @term’`. @@ -465,8 +465,8 @@ to apply specific treatments accordingly. This paragraph describes the basic form of pattern matching. See 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:`case_item` expression, an :token:`eqn` restricted to a -single :token:`pattern` and :token:`pattern` restricted to the form +by a single :n:`@case_item` expression, an :n:`@eqn` restricted to a +single :n:`@pattern` and :n:`@pattern` restricted to the form :n:`@qualid {* @ident}`. The expression @@ -488,7 +488,7 @@ In the *dependent* case, there are three subcases. In the first subcase, the type in each branch may depend on the exact value being matched in the branch. In this case, the whole pattern matching itself depends on the term being matched. This dependency of the term being matched in the -return type is expressed with an :n:`@ident` clause where :token:`ident` +return type is expressed with an :n:`@ident` clause where :n:`@ident` is dependent in the return type. For instance, in the following example: .. coqtop:: in @@ -540,7 +540,7 @@ dependency of the return type in the annotations of the inductive type is expressed with a clause in the form :n:`in @qualid {+ _ } {+ @pattern }`, where -- :token:`qualid` is the inductive type of the term being matched; +- :n:`@qualid` is the inductive type of the term being matched; - the holes :n:`_` match the parameters of the inductive type: the return type is not dependent on them. @@ -597,13 +597,13 @@ Recursive and co-recursive functions: fix and cofix | @ @qualid {? @univ_annot } -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 +The expression “``fix`` :n:`@ident`:math:`_1` :n:`@binder`:math:`_1` ``:`` +:n:`@type`:math:`_1` ``:=`` :n:`@term`:math:`_1` ``with … with`` +:n:`@ident`:math:`_n` :n:`@binder`:math:`_n` : :n:`@type`:math:`_n` +``:=`` :n:`@term`:math:`_n` ``for`` :n:`@ident`:math:`_i`” denotes the :math:`i`-th component of a block of functions defined by mutual structural recursion. It is the local counterpart of the :cmd:`Fixpoint` command. When -:math:`n=1`, the “``for`` :token:`ident`:math:`_i`” clause is omitted. +:math:`n=1`, the “``for`` :n:`@ident`:math:`_i`” clause is omitted. The association of a single fixpoint and a local definition have a special syntax: :n:`let fix @ident @binders := @term in` stands for @@ -616,12 +616,12 @@ syntax: :n:`let fix @ident @binders := @term in` stands for | cofix @cofix_body {? {+ with @cofix_body } for @ident } cofix_body ::= @ident {* @binder } {? : @term } := @term -The expression “``cofix`` :token:`ident`:math:`_1` :token:`binder`:math:`_1` ``:`` -:token:`type`:math:`_1` ``with … with`` :token:`ident`:math:`_n` :token:`binder`:math:`_n` -: :token:`type`:math:`_n` ``for`` :token:`ident`:math:`_i`” denotes the +The expression “``cofix`` :n:`@ident`:math:`_1` :n:`@binder`:math:`_1` ``:`` +:n:`@type`:math:`_1` ``with … with`` :n:`@ident`:math:`_n` :n:`@binder`:math:`_n` +: :n:`@type`:math:`_n` ``for`` :n:`@ident`:math:`_i`” denotes the :math:`i`-th component of a block of terms defined by a mutual guarded co-recursion. It is the local counterpart of the :cmd:`CoFixpoint` command. When -:math:`n=1`, the “``for`` :token:`ident`:math:`_i`” clause is omitted. +:math:`n=1`, the “``for`` :n:`@ident`:math:`_i`” clause is omitted. .. _vernacular: @@ -670,12 +670,12 @@ Assumptions ----------- Assumptions extend the environment with axioms, parameters, hypotheses -or variables. An assumption binds an :token:`ident` to a :token:`type`. It is accepted -by Coq if and only if this :token:`type` is a correct type in the environment -preexisting the declaration and if :token:`ident` was not previously defined in -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`. +or variables. An assumption binds an :n:`@ident` to a :n:`@type`. It is accepted +by Coq if and only if this :n:`@type` is a correct type in the environment +preexisting the declaration and if :n:`@ident` was not previously defined in +the same module. This :n:`@type` is considered to be the type (or +specification, or statement) assumed by :n:`@ident` and we say that :n:`@ident` +has type :n:`@type`. .. _Axiom: @@ -685,23 +685,20 @@ has type :token:`type`. .. insertprodn assumption_token of_type .. prodn:: - assumption_token ::= Axiom - | Conjecture - | Hypothesis - | Parameter - | Variable - | Axioms - | Conjectures - | Hypotheses - | Parameters - | Variables + assumption_token ::= {| Axiom | Axioms } + | {| Conjecture | Conjectures } + | {| Parameter | Parameters } + | {| Hypothesis | Hypotheses } + | {| Variable | Variables } assumpt ::= {+ @ident_decl } @of_type ident_decl ::= @ident {? @univ_decl } of_type ::= {| : | :> | :>> } @term - This command links :token:`type` to the name :token:`ident` as its specification in - the global context. The fact asserted by :token:`type` is thus assumed as a - postulate. + This command links :n:`@type` to the name :n:`@ident` as its specification in + the global context. The fact asserted by :n:`@type` is thus assumed as a + postulate. :n:`Axiom`, :n:`Conjecture`, :n:`Parameter` and their plural forms + are equivalent. Similarly, :n:`Hypothesis`, :n:`Variable` and their plural forms + are equivalent. .. exn:: @ident already exists. :name: @ident already exists. (Axiom) @@ -709,7 +706,7 @@ has type :token:`type`. .. cmdv:: Parameter {+ @ident } : @type - Adds several parameters with specification :token:`type`. + Adds several parameters with specification :n:`@type`. .. cmdv:: Parameter {+ ( {+ @ident } : @type ) } @@ -722,22 +719,10 @@ has type :token:`type`. :cmd:`Import` and its variants. You have to explicitly give their fully qualified name to refer to them. - .. cmdv:: {? Local } Parameters {+ ( {+ @ident } : @type ) } - {? Local } Axiom {+ ( {+ @ident } : @type ) } - {? Local } Axioms {+ ( {+ @ident } : @type ) } - {? Local } Conjecture {+ ( {+ @ident } : @type ) } - {? Local } Conjectures {+ ( {+ @ident } : @type ) } - :name: ParametersVar; AxiomVar; AxiomsVar; ConjectureVar; ConjecturesVar + .. cmdv:: Variable {+ ( {+ @ident } : @type ) } + :name: Variable (outside a section) - These variants are synonyms of :n:`{? Local } Parameter {+ ( {+ @ident } : @type ) }`. - - .. cmdv:: Variable {+ ( {+ @ident } : @type ) } - Variables {+ ( {+ @ident } : @type ) } - Hypothesis {+ ( {+ @ident } : @type ) } - Hypotheses {+ ( {+ @ident } : @type ) } - :name: Variable (outside a section); Variables (outside a section); Hypothesis (outside a section); Hypotheses (outside a section) - - Outside of any section, these variants are synonyms of + Outside of any section, this variant is equivalent to :n:`Local Parameter {+ ( {+ @ident } : @type ) }`. For their meaning inside a section, see :cmd:`Variable` in :ref:`section-mechanism`. @@ -750,7 +735,7 @@ has type :token:`type`. .. note:: It is advised to use the commands :cmd:`Axiom`, :cmd:`Conjecture` and :cmd:`Hypothesis` (and their plural forms) for logical postulates (i.e. when - the assertion :token:`type` is of sort :g:`Prop`), and to use the commands + the assertion :n:`@type` is of sort :g:`Prop`), and to use the commands :cmd:`Parameter` and :cmd:`Variable` (and their plural forms) in other cases (corresponding to the declaration of an abstract mathematical entity). @@ -777,19 +762,20 @@ type which is the type of its body. A formal presentation of constants and environments is given in Section :ref:`typing-rules`. -.. cmd:: @def_token @ident_decl @def_body - :name: Definition; Example; SubClass +.. cmd:: {| Definition | Example } @ident_decl @def_body + :name: Definition; Example - .. insertprodn def_token pattern_occ + .. insertprodn def_body reduce .. prodn:: - def_token ::= Definition - | Example - | SubClass def_body ::= {* @binder } := {? @reduce } @term | {* @binder } : @term := {? @reduce } @term | {* @binder } : @term reduce ::= Eval @red_expr in + + .. insertgram red_expr pattern_occ + + .. prodn:: red_expr ::= red | hnf | simpl {? @delta_flag } {? @ref_or_pattern_occ } @@ -827,8 +813,8 @@ Section :ref:`typing-rules`. unfold_occ ::= @smart_global {? at @occs_nums } pattern_occ ::= @term1_extended {? at @occs_nums } - This command binds :token:`term` to the name :token:`ident` in the environment, - provided that :token:`term` is well-typed. + This command binds :n:`@term` to the name :n:`@ident` in the environment, + provided that :n:`@term` is well-typed. .. exn:: @ident already exists. :name: @ident already exists. (Definition) @@ -836,9 +822,9 @@ Section :ref:`typing-rules`. .. cmdv:: Definition @ident : @type := @term - This variant checks that the type of :token:`term` is definitionally equal to - :token:`type`, and registers :token:`ident` as being of type - :token:`type`, and bound to value :token:`term`. + This variant checks that the type of :n:`@term` is definitionally equal to + :n:`@type`, and registers :n:`@ident` as being of type + :n:`@type`, and bound to value :n:`@term`. .. exn:: The term @term has type @type while it is expected to have type @type'. :undocumented: @@ -856,7 +842,6 @@ Section :ref:`typing-rules`. You have to explicitly give their fully qualified name to refer to them. .. cmdv:: {? Local } Example @ident {? @binders } {? : @type } := @term - :name: ExampleVar This is equivalent to :cmd:`Definition`. @@ -891,19 +876,19 @@ Simple inductive types .. cmd:: Inductive @ident : {? @sort } := {? | } @ident : @type {* | @ident : @type } This command defines a simple inductive type and its constructors. - The first :token:`ident` is the name of the inductively defined type - and :token:`sort` is the universe where it lives. The next :token:`ident`\s - are the names of its constructors and :token:`type` their respective types. - Depending on the universe where the inductive type :token:`ident` lives - (e.g. its type :token:`sort`), Coq provides a number of destructors. - Destructors are named :token:`ident`\ ``_sind``, :token:`ident`\ ``_ind``, - :token:`ident`\ ``_rec`` or :token:`ident`\ ``_rect`` which respectively + The first :n:`@ident` is the name of the inductively defined type + and :n:`@sort` is the universe where it lives. The next :n:`@ident`\s + are the names of its constructors and :n:`@type` their respective types. + Depending on the universe where the inductive type :n:`@ident` lives + (e.g. its type :n:`@sort`), Coq provides a number of destructors. + Destructors are named :n:`@ident`\ ``_sind``, :n:`@ident`\ ``_ind``, + :n:`@ident`\ ``_rec`` or :n:`@ident`\ ``_rect`` which respectively correspond to elimination principles on :g:`SProp`, :g:`Prop`, :g:`Set` and :g:`Type`. The type of the destructors expresses structural induction/recursion - principles over objects of type :token:`ident`. - The constant :token:`ident`\ ``_ind`` is always provided, - whereas :token:`ident`\ ``_rec`` and :token:`ident`\ ``_rect`` can be - impossible to derive (for example, when :token:`ident` is a proposition). + principles over objects of type :n:`@ident`. + The constant :n:`@ident`\ ``_ind`` is always provided, + whereas :n:`@ident`\ ``_rec`` and :n:`@ident`\ ``_rect`` can be + impossible to derive (for example, when :n:`@ident` is a proposition). .. exn:: Non strictly positive occurrence of @ident in @type. @@ -915,7 +900,7 @@ Simple inductive types .. exn:: The conclusion of @type is not valid; it must be built from @ident. The conclusion of the type of the constructors must be the inductive type - :token:`ident` being defined (or :token:`ident` applied to arguments in + :n:`@ident` being defined (or :n:`@ident` applied to arguments in the case of annotated inductive types — cf. next section). .. example:: @@ -951,7 +936,7 @@ Simple inductive types .. cmdv:: Inductive @ident {? : @sort } := {? | } {*| @ident {? @binders } {? : @type } } - Constructors :token:`ident`\s can come with :token:`binders` in which case, + Constructors :n:`@ident`\s can come with :n:`@binders` in which case, the actual type of the constructor is :n:`forall @binders, @type`. In the case where inductive types have no annotations (next section @@ -1012,7 +997,7 @@ Parameterized inductive types instance of the predicate :g:`even`. In some cases, all the constructors introduce the same generic instance of the inductive definition, in which case, instead of an annotation, we use a context of parameters - which are :token:`binders` shared by all the constructors of the definition. + which are :n:`@binders` shared by all the constructors of the definition. Parameters differ from inductive type annotations in the fact that the conclusion of each type of constructor invoke the inductive type with @@ -1134,14 +1119,14 @@ Mutually defined inductive types This variant allows defining a block of mutually inductive types. It has the same semantics as the above :cmd:`Inductive` definition for each - :token:`ident`. All :token:`ident` are simultaneously added to the environment. - Then well-typing of constructors can be checked. Each one of the :token:`ident` + :n:`@ident`. All :n:`@ident` are simultaneously added to the environment. + Then well-typing of constructors can be checked. Each one of the :n:`@ident` can be used on its own. .. cmdv:: Inductive @ident @binders {? : @type } := {? | } {*| @ident : @type } {* with {? | } {*| @ident @binders {? : @type } } } In this variant, the inductive definitions are parameterized - with :token:`binders`. However, parameters correspond to a local context + with :n:`@binders`. However, parameters correspond to a local context in which the whole set of inductive declarations is done. For this reason, the parameters must be strictly the same for each inductive types. @@ -1329,15 +1314,15 @@ constructions. .. prodn:: fix_definition ::= @ident_decl {* @binder } {? @fixannot } {? : @term } {? := @term } {? @decl_notations } - decl_notations ::= where {+and @decl_notation } + decl_notations ::= where @decl_notation {* and @decl_notation } decl_notation ::= @string := @term1_extended {? : @ident } 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 :token:`binders` such that :token:`ident` applied to arguments - corresponding to these :token:`binders` has type :token:`type`, and is - equivalent to the expression :token:`term`. The type of :token:`ident` is + to define :n:`@ident` a recursive function with arguments specified by + the :n:`@binders` such that :n:`@ident` applied to arguments + corresponding to these :n:`@binders` has type :n:`@type`, and is + equivalent to the expression :n:`@term`. The type of :n:`@ident` is consequently :n:`forall @binders, @type` and its value is equivalent to :n:`fun @binders => @term`. @@ -1537,9 +1522,9 @@ Chapter :ref:`Tactics`. The basic assertion command is: | Property After the statement is asserted, Coq needs a proof. Once a proof of - :token:`type` under the assumptions represented by :token:`binders` is given and + :n:`@type` under the assumptions represented by :n:`@binders` is given and validated, the proof is generalized into a proof of :n:`forall @binders, @type` and - the theorem is bound to the name :token:`ident` in the environment. + the theorem is bound to the name :n:`@ident` in the environment. .. exn:: The term @term has type @type which should be Set, Prop or Type. :undocumented: @@ -1577,7 +1562,7 @@ Chapter :ref:`Tactics`. The basic assertion command is: .. cmdv:: Definition @ident {? @binders } : @type - This allows defining a term of type :token:`type` using the proof editing + This allows defining a term of type :n:`@type` using the proof editing mode. It behaves as :cmd:`Theorem` but is intended to be used in conjunction with :cmd:`Defined` in order to define a constant of which the computational behavior is relevant. @@ -1645,7 +1630,7 @@ between ``#[`` (hash and opening square bracket) and ``]`` (closing square brack and separated by commas ``,``. Multiple space-separated blocks may be provided. Each attribute has a name (an identifier) and may have a value. -A value is either a :token:`string` (in which case it is specified with an equal ``=`` sign), +A value is either a :n:`@string` (in which case it is specified with an equal ``=`` sign), or a list of attributes, enclosed within brackets. Some attributes are specific to a command, and so are described with diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index dbe714c3888b1..8b9168977c057 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -357,7 +357,7 @@ Thanks to reserved notations, the inductive, co-inductive, record, recursive and corecursive definitions can benefit from 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, +definitions). The exact syntax is given by :n:`@decl_notation` for inductive, co-inductive, recursive and corecursive definitions and in :ref:`record-types` for records. Here are examples: @@ -873,7 +873,6 @@ notations are given below. The optional :production:`scope` is described in : Fixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`]. : CoFixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`]. : [Local] Declare Custom Entry `ident`. - decl_notation : [where `string` := `term` [: `scope`] and … and `string` := `term` [: `scope`]]. modifiers : `modifier`, … , `modifier` modifier : at level `num` : in custom `ident` diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 38fb598acd888..72fbebd1ea98b 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -374,10 +374,27 @@ evar_instance: [ gallina: [ | DELETE assumptions_token inline assum_list +| REPLACE OPT cumulativity_token private_token finite_token LIST1 inductive_definition SEP "with" +| WITH OPT cumulativity_token private_token finite_token inductive_definition LIST0 ( "with" inductive_definition ) +| REPLACE "Fixpoint" LIST1 rec_definition SEP "with" +| WITH "Fixpoint" rec_definition LIST0 ( "with" rec_definition ) +| REPLACE "Let" "Fixpoint" LIST1 rec_definition SEP "with" +| WITH "Let" "Fixpoint" rec_definition LIST0 ( "with" rec_definition ) +| REPLACE "CoFixpoint" LIST1 corec_definition SEP "with" +| WITH "CoFixpoint" corec_definition LIST0 ( "with" corec_definition ) +| REPLACE "Let" "CoFixpoint" LIST1 corec_definition SEP "with" +| WITH "Let" "CoFixpoint" corec_definition LIST0 ( "with" corec_definition ) +| REPLACE "Scheme" LIST1 scheme SEP "with" +| WITH "Scheme" scheme LIST0 ( "with" scheme ) ] -assumption_token: [ -| assumptions_token +decl_notation: [ +| REPLACE "where" LIST1 one_decl_notation SEP decl_sep +| WITH "where" one_decl_notation LIST0 ( decl_sep one_decl_notation ) +] + +assumptions_token: [ +| DELETENT ] inline: [ @@ -615,6 +632,14 @@ printable: [ command: [ | REPLACE "Print" printable | WITH printable +| "SubClass" ident_decl def_body +| REPLACE "Ltac" LIST1 ltac_tacdef_body SEP "with" +| WITH "Ltac" ltac_tacdef_body LIST0 ( "with" ltac_tacdef_body ) +| REPLACE "Function" LIST1 function_rec_definition_loc SEP "with" (* funind plugin *) +| WITH "Function" function_rec_definition_loc LIST0 ( "with" function_rec_definition_loc ) (* funind plugin *) +| REPLACE "Functional" "Scheme" LIST1 fun_scheme_arg SEP "with" (* funind plugin *) +| WITH "Functional" "Scheme" fun_scheme_arg LIST0 ( "with" fun_scheme_arg ) (* funind plugin *) + ] only_parsing: [ @@ -642,7 +667,7 @@ decl_notation: [ binder_tactic: [ | REPLACE "let" [ "rec" | ] LIST1 let_clause SEP "with" "in" tactic_expr5 -| WITH "let" OPT "rec" LIST1 let_clause SEP "with" "in" tactic_expr5 +| WITH "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" tactic_expr5 ] tactic_then_gen: [ @@ -672,6 +697,23 @@ vernac_aux: [ | tactic_mode "." ] +def_token: [ +| DELETE "SubClass" (* document separately from Definition and Example *) +] + +assumption_token: [ +| REPLACE "Axiom" +| WITH [ "Axiom" | "Axioms" ] +| REPLACE "Conjecture" +| WITH [ "Conjecture" | "Conjectures" ] +| REPLACE "Hypothesis" +| WITH [ "Hypothesis" | "Hypotheses" ] +| REPLACE "Parameter" +| WITH [ "Parameter" | "Parameters" ] +| REPLACE "Variable" +| WITH [ "Variable" | "Variables" ] +] + SPLICE: [ | noedit_mode | command_entry @@ -787,7 +829,6 @@ SPLICE: [ | evar_instance | fix_decls | cofix_decls -| assumptions_token | assum_list | assum_coe | inline @@ -804,6 +845,7 @@ SPLICE: [ | quoted_attributes (* todo: splice or not? *) | printable | only_parsing +| def_token ] (* end SPLICE *) RENAME: [ diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml index 7d18630a02ff7..5fcb56f5f2ca3 100644 --- a/doc/tools/docgram/doc_grammar.ml +++ b/doc/tools/docgram/doc_grammar.ml @@ -1700,9 +1700,9 @@ let process_rst g file args seen tac_prods cmd_prods = let start_index = index_of start !g.order in let end_index = index_of end_ !g.order in if start_index = None then - error "%s line %d: '%s' is undefined\n" file !linenum start; + error "%s line %d: '%s' is undefined in insertprodn\n" file !linenum start; if end_index = None then - error "%s line %d: '%s' is undefined\n" file !linenum end_; + error "%s line %d: '%s' is undefined in insertprodn\n" file !linenum end_; if start_index <> None && end_index <> None then check_range_consistency g start end_; match start_index, end_index with diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index ba8114f53ab3e..c784582d434ce 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -124,16 +124,11 @@ record_binder_body: [ ] assumption_token: [ -| "Axiom" -| "Conjecture" -| "Hypothesis" -| "Parameter" -| "Variable" -| "Axioms" -| "Conjectures" -| "Hypotheses" -| "Parameters" -| "Variables" +| [ "Axiom" | "Axioms" ] +| [ "Conjecture" | "Conjectures" ] +| [ "Parameter" | "Parameters" ] +| [ "Hypothesis" | "Hypotheses" ] +| [ "Variable" | "Variables" ] ] assumpt: [ @@ -378,14 +373,14 @@ subprf: [ gallina: [ | thm_token ident_decl LIST0 binder ":" term LIST0 [ "with" ident_decl LIST0 binder ":" term ] | assumption_token OPT ( "Inline" OPT ( "(" num ")" ) ) [ LIST1 ( "(" assumpt ")" ) | assumpt ] -| def_token ident_decl def_body +| [ "Definition" | "Example" ] ident_decl def_body | "Let" ident def_body -| OPT cumulativity_token private_token finite_token LIST1 inductive_definition SEP "with" -| "Fixpoint" LIST1 fix_definition SEP "with" -| "Let" "Fixpoint" LIST1 fix_definition SEP "with" -| "CoFixpoint" LIST1 cofix_definition SEP "with" -| "Let" "CoFixpoint" LIST1 cofix_definition SEP "with" -| "Scheme" LIST1 scheme SEP "with" +| OPT cumulativity_token private_token finite_token inductive_definition LIST0 ( "with" inductive_definition ) +| "Fixpoint" fix_definition LIST0 ( "with" fix_definition ) +| "Let" "Fixpoint" fix_definition LIST0 ( "with" fix_definition ) +| "CoFixpoint" cofix_definition LIST0 ( "with" cofix_definition ) +| "Let" "CoFixpoint" cofix_definition LIST0 ( "with" cofix_definition ) +| "Scheme" scheme LIST0 ( "with" scheme ) | "Combined" "Scheme" ident "from" LIST1 ident SEP "," | "Register" qualid "as" qualid | "Register" "Inline" qualid @@ -400,7 +395,7 @@ fix_definition: [ ] decl_notations: [ -| "where" LIST1 decl_notation SEP "and" +| "where" decl_notation LIST0 ( "and" decl_notation ) ] decl_notation: [ @@ -468,12 +463,6 @@ thm_token: [ | "Property" ] -def_token: [ -| "Definition" -| "Example" -| "SubClass" -] - def_body: [ | LIST0 binder ":=" OPT reduce term | LIST0 binder ":" term ":=" OPT reduce term @@ -996,12 +985,12 @@ command: [ | "Print" "Rewrite" "HintDb" ident | "Print" "Ltac" qualid | "Locate" "Ltac" qualid -| "Ltac" LIST1 tacdef_body SEP "with" +| "Ltac" tacdef_body LIST0 ( "with" tacdef_body ) | "Print" "Ltac" "Signatures" | "Set" "Firstorder" "Solver" ltac_expr | "Print" "Firstorder" "Solver" -| "Function" LIST1 fix_definition SEP "with" (* funind plugin *) -| "Functional" "Scheme" LIST1 fun_scheme_arg SEP "with" (* funind plugin *) +| "Function" fix_definition LIST0 ( "with" fix_definition ) +| "Functional" "Scheme" fun_scheme_arg LIST0 ( "with" fun_scheme_arg ) | "Extraction" qualid (* extraction plugin *) | "Recursive" "Extraction" LIST1 qualid (* extraction plugin *) | "Extraction" string LIST1 qualid (* extraction plugin *) @@ -1041,6 +1030,7 @@ command: [ | "Print" "Fields" (* setoid_ring plugin *) | "Numeral" "Notation" qualid qualid qualid ":" ident OPT numnotoption | "String" "Notation" qualid qualid qualid ":" ident +| "SubClass" ident_decl def_body ] orient: [ @@ -1952,7 +1942,7 @@ ltac_expr: [ binder_tactic: [ | "fun" LIST1 fun_var "=>" ltac_expr -| "let" OPT "rec" LIST1 let_clause SEP "with" "in" ltac_expr +| "let" OPT "rec" let_clause LIST0 ( "with" let_clause ) "in" ltac_expr | "info" ltac_expr ]