diff options
Diffstat (limited to 'doc/sphinx/user-extensions')
| -rw-r--r-- | doc/sphinx/user-extensions/proof-schemes.rst | 34 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 278 |
2 files changed, 176 insertions, 136 deletions
diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index 838926d651..ab1edc0b27 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -40,8 +40,7 @@ induction for objects in type `identᵢ`. Induction scheme for tree and forest. - The definition of principle of mutual induction for tree and forest - over the sort Set is defined by the command: + A mutual induction principle for tree and forest in sort ``Set`` can be defined using the command .. coqtop:: none @@ -193,10 +192,12 @@ command generates the induction principle for each `identᵢ`, following the recursive structure and case analyses of the corresponding function identᵢ’. -Remark: There is a difference between obtaining an induction scheme by -using ``Functional Scheme`` on a function defined by ``Function`` or not. -Indeed, ``Function`` generally produces smaller principles, closer to the -definition written by the user. +.. warning:: + + There is a difference between induction schemes generated by the command + :cmd:`Functional Scheme` and these generated by the :cmd:`Function`. Indeed, + :cmd:`Function` generally produces smaller principles that are closer to how + a user would implement them. See :ref:`advanced-recursive-functions` for details. .. example:: @@ -257,11 +258,6 @@ definition written by the user. auto with arith. Qed. - Remark: There is a difference between obtaining an induction scheme - for a function by using ``Function`` (see :ref:`advanced-recursive-functions`) and by using - ``Functional Scheme`` after a normal definition using ``Fixpoint`` or - ``Definition``. See :ref:`advanced-recursive-functions` for details. - .. example:: Induction scheme for tree_size. @@ -298,15 +294,15 @@ definition written by the user. | cons t f' => (tree_size t + forest_size f') end. - Remark: Function generates itself non mutual induction principles - tree_size_ind and forest_size_ind: + Notice that the induction principles ``tree_size_ind`` and ``forest_size_ind`` + generated by ``Function`` are not mutual. .. coqtop:: all Check tree_size_ind. - The definition of mutual induction principles following the recursive - structure of `tree_size` and `forest_size` is defined by the command: + Mutual induction principles following the recursive structure of ``tree_size`` + and ``forest_size`` can be generated by the following command: .. coqtop:: all @@ -352,10 +348,8 @@ having inverted the instance with the tactic `inversion`. .. example:: - Let us consider the relation `Le` over natural numbers and the following - variable: - - .. original LaTeX had "Variable" instead of "Axiom", which generates an ugly warning + Consider the relation `Le` over natural numbers and the following + parameter ``P``: .. coqtop:: all @@ -363,7 +357,7 @@ having inverted the instance with the tactic `inversion`. | LeO : forall n:nat, Le 0 n | LeS : forall n m:nat, Le n m -> Le (S n) (S m). - Axiom P : nat -> nat -> Prop. + Parameter P : nat -> nat -> Prop. To generate the inversion lemma for the instance `(Le (S n) m)` and the sort `Prop`, we do: diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 37394386e6..d92b9a6794 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -50,11 +50,11 @@ A notation is always surrounded by double quotes (except when the abbreviation has the form of an ordinary applicative expression; see :ref:`Abbreviations`). The notation is composed of *tokens* separated by spaces. Identifiers in the string (such as ``A`` and ``B``) are the *parameters* -of the notation. They must occur at least once each in the denoted term. The +of the notation. Each of them must occur at least once in the denoted term. The other elements of the string (such as ``/\``) are the *symbols*. An identifier can be used as a symbol but it must be surrounded by -simple quotes to avoid the confusion with a parameter. Similarly, +single quotes to avoid the confusion with a parameter. Similarly, every symbol of at least 3 characters and starting with a simple quote must be quoted (then it starts by two single quotes). Here is an example. @@ -119,7 +119,7 @@ command understands. Here is how the previous examples refine. Notation "A /\ B" := (and A B) (at level 80, right associativity). Notation "A \/ B" := (or A B) (at level 85, right associativity). -By default, a notation is considered non associative, but the +By default, a notation is considered non-associative, but the precedence level is mandatory (except for special cases whose level is canonical). The level is either a number or the phrase ``next level`` whose meaning is obvious. @@ -139,7 +139,7 @@ instance define prefix notations. Notation "~ x" := (not x) (at level 75, right associativity). One can also define notations for incomplete terms, with the hole -expected to be inferred at typing time. +expected to be inferred during typechecking. .. coqtop:: in @@ -185,14 +185,14 @@ rules. Some simple left factorization work has to be done. Here is an example. Notation "x < y" := (lt x y) (at level 70). Notation "x < y < z" := (x < y /\ y < z) (at level 70). -In order to factorize the left part of the rules, the sub-expression -referred by ``y`` has to be at the same level in both rules. However the +In order to factorize the left part of the rules, the subexpression +referred to by ``y`` has to be at the same level in both rules. However the default behavior puts ``y`` at the next level below 70 in the first rule -(``no associativity`` is the default), and at the level 200 in the second +(``no associativity`` is the default), and at level 200 in the second rule (``level 200`` is the default for inner expressions). To fix this, we need to force the parsing level of ``y``, as follows. -.. coqtop:: all +.. coqtop:: in Notation "x < y" := (lt x y) (at level 70). Notation "x < y < z" := (x < y /\ y < z) (at level 70, y at next level). @@ -283,7 +283,7 @@ the possible following elements delimited by single quotes: (4 spaces in the example) - well-bracketed pairs of tokens of the form ``'[hv '`` and ``']'`` are - translated into horizontal-orelse-vertical printing boxes; if the + translated into horizontal-or-else-vertical printing boxes; if the content of the box does not fit on a single line, then every breaking point forces a newline and an extra indentation of the number of spaces given after the “ ``[``” is applied at the beginning of each @@ -295,7 +295,7 @@ the possible following elements delimited by single quotes: of the box, and an extra indentation of the number of spaces given after the “``[``” is applied at the beginning of each newline -Notations do not survive the end of sections. No typing of the denoted +Notations disappear when a section is closed. No typing of the denoted expression is performed at definition time. Type-checking is done only at the time of use of the notation. @@ -350,7 +350,7 @@ 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 +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, @@ -359,17 +359,23 @@ for records. Here are examples: .. coqtop:: in - Inductive and (A B:Prop) : Prop := conj : A -> B -> A /\ B - where "A /\ B" := (and A B). + Reserved Notation "A & B" (at level 80). + +.. coqtop:: in + + Inductive and' (A B : Prop) : Prop := conj' : A -> B -> A & B + where "A & B" := (and' A B). + +.. coqtop:: in - Fixpoint plus (n m:nat) {struct n} : nat := - match n with - | O => m - | S p => S (p+m) - end + Fixpoint plus (n m : nat) {struct n} : nat := + match n with + | O => m + | S p => S (p+m) + end where "n + m" := (plus n m). -Displaying informations about notations +Displaying information about notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. opt:: Printing Notations @@ -565,7 +571,7 @@ confused with the three-dots notation “``…``” used in this manual to denot a sequence of arbitrary size. On the left-hand side, the part “``x s .. s y``” of the notation parses -any number of times (but at least one time) a sequence of expressions +any number of times (but at least once) a sequence of expressions separated by the sequence of tokens ``s`` (in the example, ``s`` is just “``;``”). The right-hand side must contain a subterm of the form either @@ -608,7 +614,7 @@ Notations with recursive patterns involving binders Recursive notations can also be used with binders. The basic example is: -.. coqtop:: all +.. coqtop:: in Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..)) @@ -627,7 +633,7 @@ repeatedly nested as many times as the number of binders generated. If ever the generalization operator ``'`` (see :ref:`implicit-generalization`) is used in the binding list, the added binders are taken into account too. -Binders parsing exist in two flavors. If ``x`` and ``y`` are marked as binder, +There are two flavors of binder parsing. If ``x`` and ``y`` are marked as binder, then a sequence such as :g:`a b c : T` will be accepted and interpreted as the sequence of binders :g:`(a:T) (b:T) (c:T)`. For instance, in the notation above, the syntax :g:`exists a b : nat, a = b` is valid. @@ -698,42 +704,46 @@ Custom entries This command allows to define new grammar entries, called *custom entries*, that can later be referred to using the entry name - :n:`custom @ident`. For instance, we may want to define an ad hoc - parser for arithmetical operations and proceed as follows: + :n:`custom @ident`. -.. coqtop:: all +.. example:: - Inductive Expr := - | One : Expr - | Mul : Expr -> Expr -> Expr - | Add : Expr -> Expr -> Expr. + For instance, we may want to define an ad hoc + parser for arithmetical operations and proceed as follows: - Declare Custom Entry expr. - Notation "[ e ]" := e (e custom expr at level 2). - Notation "1" := One (in custom expr at level 0). - Notation "x y" := (Mul x y) (in custom expr at level 1, left associativity). - Notation "x + y" := (Add x y) (in custom expr at level 2, left associativity). - Notation "( x )" := x (in custom expr, x at level 2). - Notation "{ x }" := x (in custom expr, x constr). - Notation "x" := x (in custom expr at level 0, x ident). - - Axiom f : nat -> Expr. - Check fun x y z => [1 + y z + {f x}]. - Unset Printing Notations. - Check fun x y z => [1 + y z + {f x}]. - Set Printing Notations. - Check fun e => match e with - | [1 + 1] => [1] - | [x y + z] => [x + y z] - | y => [y + e] - end. + .. coqtop:: all + + Inductive Expr := + | One : Expr + | Mul : Expr -> Expr -> Expr + | Add : Expr -> Expr -> Expr. + + Declare Custom Entry expr. + Notation "[ e ]" := e (e custom expr at level 2). + Notation "1" := One (in custom expr at level 0). + Notation "x y" := (Mul x y) (in custom expr at level 1, left associativity). + Notation "x + y" := (Add x y) (in custom expr at level 2, left associativity). + Notation "( x )" := x (in custom expr, x at level 2). + Notation "{ x }" := x (in custom expr, x constr). + Notation "x" := x (in custom expr at level 0, x ident). + + Axiom f : nat -> Expr. + Check fun x y z => [1 + y z + {f x}]. + Unset Printing Notations. + Check fun x y z => [1 + y z + {f x}]. + Set Printing Notations. + Check fun e => match e with + | [1 + 1] => [1] + | [x y + z] => [x + y z] + | y => [y + e] + end. Custom entries have levels, like the main grammar of terms and grammar of patterns have. The lower level is 0 and this is the level used by default to put rules delimited with tokens on both ends. The level is -left to be inferred by Coq when using :n:`in custom @ident``. The -level is otherwise given explicitly by using the syntax :n:`in custom -@ident at level @num`, where :n:`@num` refers to the level. +left to be inferred by Coq when using :n:`in custom @ident`. The +level is otherwise given explicitly by using the syntax +:n:`in custom @ident at level @num`, where :n:`@num` refers to the level. Levels are cumulative: a notation at level ``n`` of which the left end is a term shall use rules at level less than ``n`` to parse this @@ -745,16 +755,26 @@ the right end is a term shall use by default rules at level strictly less than ``n`` to parse this sub-term if the rule is declared left associative and rules at level less or equal than ``n`` if the rule is declared right associative. This is what happens for instance in the -rule ``Notation "x + y" := (Add x y) (in custom expr at level 2, left -associativity)`` where ``x`` is any expression parsed in entry +rule + +.. coqtop:: in + + Notation "x + y" := (Add x y) (in custom expr at level 2, left associativity). + +where ``x`` is any expression parsed in entry ``expr`` at level less or equal than ``2`` (including, recursively, the given rule) and ``y`` is any expression parsed in entry ``expr`` at level strictly less than ``2``. Rules associated to an entry can refer different sub-entries. The grammar entry name ``constr`` can be used to refer to the main grammar -of term as in the rule ``Notation "{ x }" := x (in custom expr at -level 0, x constr)`` which indicates that the subterm ``x`` should be +of term as in the rule + +.. coqtop:: in + + Notation "{ x }" := x (in custom expr at level 0, x constr). + +which indicates that the subterm ``x`` should be parsed using the main grammar. If not indicated, the level is computed as for notations in ``constr``, e.g. using 200 as default level for inner sub-expressions. The level can otherwise be indicated explicitly @@ -763,10 +783,19 @@ level``. Conversely, custom entries can be used to parse sub-expressions of the main grammar, or from another custom entry as is the case in -:g:`Notation "[ e ]" := e (e custom expr at level 2)` to indicate that -``e`` has to be parsed at level ``2`` of the grammar associated to the -custom entry ``expr``. The level can be omitted, as in :g:`Notation "[ e -]" := e (e custom expr)`, in which case Coq tries to infer it. + +.. coqtop:: in + + Notation "[ e ]" := e (e custom expr at level 2). + +to indicate that ``e`` has to be parsed at level ``2`` of the grammar +associated to the custom entry ``expr``. The level can be omitted, as in + +.. coqtop:: in + + Notation "[ e ]" := e (e custom expr)`. + +in which case Coq tries to infer it. In the absence of an explicit entry for parsing or printing a sub-expression of a notation in a custom entry, the default is to @@ -779,23 +808,40 @@ level n``. In general, rules are required to be *productive* on the right-hand side, i.e. that they are bound to an expression which is not reduced to a single variable. If the rule is not productive on the -right-hand side, as it is the case above for :g:`Notation "( x )" := x -(in custom expr at level 0, x at level 2)` and :g:`Notation "{ x }" := -x (in custom expr at level 0, x constr)`, it is used as a *grammar -coercion* which means that it is used to parse or print an expression -which is not available in the current grammar at the current level of -parsing or printing for this grammar but which is available in another -grammar or in another level of the current grammar. For instance, -:g:`Notation "( x )" := x (in custom expr at level 0, x at level 2)` +right-hand side, as it is the case above for + +.. coqtop:: in + + Notation "( x )" := x (in custom expr at level 0, x at level 2). + +and + +.. coqtop:: in + + Notation "{ x }" := x (in custom expr at level 0, x constr). + +it is used as a *grammar coercion* which means that it is used to parse or +print an expression which is not available in the current grammar at the +current level of parsing or printing for this grammar but which is available +in another grammar or in another level of the current grammar. For instance, + +.. coqtop:: in + + Notation "( x )" := x (in custom expr at level 0, x at level 2). + tells that parentheses can be inserted to parse or print an expression declared at level ``2`` of ``expr`` whenever this expression is expected to be used as a subterm at level 0 or 1. This allows for instance to parse and print :g:`Add x y` as a subterm of :g:`Mul (Add -x y) z` using the syntax ``(x + y) z``. Similarly, :g:`Notation "{ x }" -:= x (in custom expr at level 0, x constr)` gives a way to let any -arbitrary expression which is not in handled by the custom entry -``expr`` be parsed or printed by the main grammar of term up to the -insertion of a pair of curly brackets. +x y) z` using the syntax ``(x + y) z``. Similarly, + +.. coqtop:: in + + Notation "{ x }" := x (in custom expr at level 0, x constr). + +gives a way to let any arbitrary expression which is not handled by the +custom entry ``expr`` be parsed or printed by the main grammar of term +up to the insertion of a pair of curly brackets. .. cmd:: Print Grammar @ident. @@ -876,7 +922,7 @@ notations are given below. The optional :production:`scope` is described in Persistence of notations ++++++++++++++++++++++++ -Neither notations nor custom entries survive the end of sections. +Notations disappear when a section is closed. .. cmd:: Local Notation @notation @@ -894,9 +940,9 @@ Interpretation scopes ---------------------- An *interpretation scope* is a set of notations for terms with their -interpretation. Interpretation scopes provide a weak, purely -syntactical form of notations overloading: the same notation, for -instance the infix symbol ``+`` can be used to denote distinct +interpretations. Interpretation scopes provide a weak, purely +syntactical form of notation overloading: the same notation, for +instance the infix symbol ``+``, can be used to denote distinct definitions of the additive operator. Depending on which interpretation scopes are currently open, the interpretation is different. Interpretation scopes can include an interpretation for numerals and @@ -907,7 +953,7 @@ See :ref:`above <NotationSyntax>` for the syntax of notations including the possibility to declare them in a given scope. Here is a typical example which declares the notation for conjunction in the scope ``type_scope``. -.. coqdoc:: +.. coqtop:: in Notation "A /\ B" := (and A B) : type_scope. @@ -917,10 +963,10 @@ declares the notation for conjunction in the scope ``type_scope``. Global interpretation rules for notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -At any time, the interpretation of a notation for term is done within +At any time, the interpretation of a notation for a term is done within a *stack* of interpretation scopes and lonely notations. In case a notation has several interpretations, the actual interpretation is the -one defined by (or in) the more recently declared (or open) lonely +one defined by (or in) the more recently declared (or opened) lonely notation (or interpretation scope) which defines this notation. Typically if a given notation is defined in some scope ``scope`` but has also an interpretation not assigned to a scope, then, if ``scope`` is open @@ -946,7 +992,7 @@ lonely notations. These scopes, in opening order, are ``core_scope``, stack by using the command :n:`Close Scope @scope`. Notice that this command does not only cancel the last :n:`Open Scope @scope` - but all the invocations of it. + but all its invocations. .. note:: ``Open Scope`` and ``Close Scope`` do not survive the end of sections where they occur. When defined outside of a section, they are exported @@ -1026,11 +1072,11 @@ Binding arguments of a constant to an interpretation scope the scope is limited to the argument itself. It does not propagate to subterms but the subterms that, after interpretation of the notation, turn to be themselves arguments of a reference are interpreted - accordingly to the arguments scopes bound to this reference. + accordingly to the argument scopes bound to this reference. .. cmdv:: Arguments @qualid : clear scopes - Arguments scopes can be cleared with :n:`Arguments @qualid : clear scopes`. + This command can be used to clear argument scopes of :token:`qualid`. .. cmdv:: Arguments @qualid {+ @name%scope} : extra scopes @@ -1152,34 +1198,34 @@ Scopes` or :cmd:`Print Scope`. ``type_scope`` This scope includes infix * for product types and infix + for sum types. It - is delimited by key ``type``, and bound to the coercion class + is delimited by the key ``type``, and bound to the coercion class ``Sortclass``, as described above. ``function_scope`` - This scope is delimited by key ``function``, and bound to the coercion class + This scope is delimited by the key ``function``, and bound to the coercion class ``Funclass``, as described above. ``nat_scope`` This scope includes the standard arithmetical operators and relations on type nat. Positive numerals in this scope are mapped to their canonical - representent built from :g:`O` and :g:`S`. The scope is delimited by key + representent built from :g:`O` and :g:`S`. The scope is delimited by the key ``nat``, and bound to the type :g:`nat` (see above). ``N_scope`` This scope includes the standard arithmetical operators and relations on - type :g:`N` (binary natural numbers). It is delimited by key ``N`` and comes + type :g:`N` (binary natural numbers). It is delimited by the key ``N`` and comes with an interpretation for numerals as closed terms of type :g:`N`. ``Z_scope`` This scope includes the standard arithmetical operators and relations on - type :g:`Z` (binary integer numbers). It is delimited by key ``Z`` and comes - with an interpretation for numerals as closed term of type :g:`Z`. + type :g:`Z` (binary integer numbers). It is delimited by the key ``Z`` and comes + with an interpretation for numerals as closed terms of type :g:`Z`. ``positive_scope`` This scope includes the standard arithmetical operators and relations on type :g:`positive` (binary strictly positive numbers). It is delimited by key ``positive`` and comes with an interpretation for numerals as closed - term of type :g:`positive`. + terms of type :g:`positive`. ``Q_scope`` This scope includes the standard arithmetical operators and relations on @@ -1196,20 +1242,20 @@ Scopes` or :cmd:`Print Scope`. ``real_scope`` This scope includes the standard arithmetical operators and relations on - type :g:`R` (axiomatic real numbers). It is delimited by key ``R`` and comes + type :g:`R` (axiomatic real numbers). It is delimited by the key ``R`` and comes with an interpretation for numerals using the :g:`IZR` morphism from binary integer numbers to :g:`R`. ``bool_scope`` - This scope includes notations for the boolean operators. It is delimited by + This scope includes notations for the boolean operators. It is delimited by the key ``bool``, and bound to the type :g:`bool` (see above). ``list_scope`` - This scope includes notations for the list operators. It is delimited by key + This scope includes notations for the list operators. It is delimited by the key ``list``, and bound to the type :g:`list` (see above). ``core_scope`` - This scope includes the notation for pairs. It is delimited by key ``core``. + This scope includes the notation for pairs. It is delimited by the key ``core``. ``string_scope`` This scope includes notation for strings as elements of the type string. @@ -1228,7 +1274,7 @@ Scopes` or :cmd:`Print Scope`. the ASCII code 34), all of them being represented in the type :g:`ascii`. -Displaying informations about scopes +Displaying information about scopes ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. cmd:: Print Visibility @@ -1236,7 +1282,7 @@ Displaying informations about scopes This displays the current stack of notations in scopes and lonely notations that is used to interpret a notation. The top of the stack is displayed last. Notations in scopes whose interpretation is hidden - by the same notation in a more recently open scope are not displayed. + by the same notation in a more recently opened scope are not displayed. Hence each notation is displayed only once. .. cmdv:: Print Visibility @scope @@ -1249,13 +1295,13 @@ Displaying informations about scopes .. cmd:: Print Scopes This displays all the notations, delimiting keys and corresponding - class of all the existing interpretation scopes. It also displays the + classes of all the existing interpretation scopes. It also displays the lonely notations. .. cmdv:: Print Scope @scope :name: Print Scope - This displays all the notations defined in interpretation scope :token:`scope`. + This displays all the notations defined in the interpretation scope :token:`scope`. It also displays the delimiting key if any and the class to which the scope is bound, if any. @@ -1297,13 +1343,13 @@ Abbreviations much as possible by the Coq printers unless the modifier ``(only parsing)`` is given. - Abbreviations are bound to an absolute name as an ordinary definition - is, and they can be referred by qualified names too. + An abbreviation is bound to an absolute name as an ordinary definition is + and it also can be referred to by a qualified name. Abbreviations are syntactic in the sense that they are bound to expressions which are not typed at the time of the definition of the - abbreviation but at the time it is used. Especially, abbreviations can - be bound to terms with holes (i.e. with “``_``”). For example: + abbreviation but at the time they are used. Especially, abbreviations + can be bound to terms with holes (i.e. with “``_``”). For example: .. coqtop:: none reset @@ -1313,13 +1359,16 @@ Abbreviations .. coqtop:: in Definition explicit_id (A:Set) (a:A) := a. + + .. coqtop:: in + Notation id := (explicit_id _). .. coqtop:: all Check (id 0). - Abbreviations do not survive the end of sections. No typing of the + Abbreviations disappear when a section is closed. No typing of the denoted expression is performed at definition time. Type-checking is done only at the time of use of the abbreviation. @@ -1328,8 +1377,7 @@ Abbreviations Tactic Notations ----------------- -Tactic notations allow to customize the syntax of the tactics of the -tactic language. Tactic notations obey the following syntax: +Tactic notations allow to customize the syntax of tactics. They have the following syntax: .. productionlist:: coq tacn : Tactic Notation [`tactic_level`] [`prod_item` … `prod_item`] := `tactic`. @@ -1351,7 +1399,7 @@ tactic language. Tactic notations obey the following syntax: a terminal symbol, i.e. a string, for the first production item. The tactic level indicates the parsing precedence of the tactic notation. This information is particularly relevant for notations of tacticals. - Levels 0 to 5 are available (default is 0). + Levels 0 to 5 are available (default is 5). .. cmd:: Print Grammar tactic @@ -1378,7 +1426,7 @@ tactic language. Tactic notations obey the following syntax: * - ``simple_intropattern`` - intro_pattern - - an intro_pattern + - an intro pattern - intros * - ``hyp`` @@ -1432,7 +1480,7 @@ tactic language. Tactic notations obey the following syntax: - .. note:: In order to be bound in tactic definitions, each syntactic - entry for argument type must include the case of simple L tac + entry for argument type must include the case of a simple |Ltac| identifier as part of what it parses. This is naturally the case for ``ident``, ``simple_intropattern``, ``reference``, ``constr``, ... but not for ``integer``. This is the reason for introducing a special entry ``int_or_var`` which @@ -1446,18 +1494,16 @@ tactic language. Tactic notations obey the following syntax: .. cmdv:: Local Tactic Notation - Tactic notations do not survive the end of sections. They survive - modules unless the command Local Tactic Notation is used instead of - Tactic Notation. + Tactic notations disappear when a section is closed. They survive when + a module is closed unless the command ``Local Tactic Notation`` is used instead + of :cmd:`Tactic Notation`. .. rubric:: Footnotes .. [#and_or_levels] which are the levels effectively chosen in the current implementation of Coq -.. [#no_associativity] Coq accepts notations declared as ``no - associativity`` but the parser on which Coq is built, namely - Camlp5, currently does not implement ``no associativity`` and - replaces it with ``left associativity``; hence it is the same for - Coq: ``no associativity`` is in fact ``left associativity``, for - the purposes of parsing +.. [#no_associativity] Coq accepts notations declared as non-associative but the parser on + which Coq is built, namely Camlp5, currently does not implement ``no associativity`` and + replaces it with ``left associativity``; hence it is the same for Coq: ``no associativity`` + is in fact ``left associativity`` for the purposes of parsing |