diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/03-notations/11841-master+distinguishing-ident-name-in-grammar-entries.rst | 13 | ||||
| -rw-r--r-- | doc/changelog/04-tactics/13417-no_int_or_var.rst | 7 | ||||
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/canonical.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 14 | ||||
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/rewriting.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 91 | ||||
| -rw-r--r-- | doc/tools/docgram/common.edit_mlg | 40 | ||||
| -rw-r--r-- | doc/tools/docgram/fullGrammar | 52 | ||||
| -rw-r--r-- | doc/tools/docgram/orderedGrammar | 53 |
11 files changed, 193 insertions, 97 deletions
diff --git a/doc/changelog/03-notations/11841-master+distinguishing-ident-name-in-grammar-entries.rst b/doc/changelog/03-notations/11841-master+distinguishing-ident-name-in-grammar-entries.rst new file mode 100644 index 0000000000..8d681361e8 --- /dev/null +++ b/doc/changelog/03-notations/11841-master+distinguishing-ident-name-in-grammar-entries.rst @@ -0,0 +1,13 @@ +- **Changed:** + In notations (except in custom entries), the misleading :n:`@syntax_modifier` + :n:`@ident ident` (which accepted either an identifier or + a :g:`_`) is deprecated and should be replaced by :n:`@ident name`. If + the intent was really to only parse identifiers, this will + eventually become possible, but only as of Coq 8.15. + In custom entries, the meaning of :n:`@ident ident` is silently changed + from parsing identifiers or :g:`_` to parsing only identifiers + without warning, but this presumably affects only rare, recent and + relatively experimental code + (`#11841 <https://github.com/coq/coq/pull/11841>`_, + fixes `#9514 <https://github.com/coq/coq/pull/9514>`_, + by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/13417-no_int_or_var.rst b/doc/changelog/04-tactics/13417-no_int_or_var.rst new file mode 100644 index 0000000000..667ee28eea --- /dev/null +++ b/doc/changelog/04-tactics/13417-no_int_or_var.rst @@ -0,0 +1,7 @@ +- **Removed:** + A number of tactics that formerly accepted negative + numbers as parameters now give syntax errors for negative + values. These include {e}constructor, do, timeout, + 9 {e}auto tactics and psatz*. + (`#13417 <https://github.com/coq/coq/pull/13417>`_, + by Jim Fehrle). diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index fb9965e43a..28b60878d2 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -250,11 +250,11 @@ proof by abstracting monomials by variables. `psatz`: a proof procedure for non-linear arithmetic ---------------------------------------------------- -.. tacn:: psatz @one_term {? @int_or_var } +.. tacn:: psatz @one_term {? @nat_or_var } :name: psatz This tactic explores the *Cone* by increasing degrees – hence the - depth parameter *n*. In theory, such a proof search is complete – if the + depth parameter :token:`nat_or_var`. In theory, such a proof search is complete – if the goal is provable the search eventually stops. Unfortunately, the external oracle is using numeric (approximate) optimization techniques that might miss a refutation. diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 22527dc379..98445fca1a 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -405,7 +405,7 @@ Summary of the commands Shows the list of instances associated with the typeclass :token:`reference`. -.. tacn:: typeclasses eauto {? bfs } {? @int_or_var } {? with {+ @ident } } +.. tacn:: typeclasses eauto {? bfs } {? @nat_or_var } {? with {+ @ident } } This proof search tactic uses the resolution engine that is run implicitly during type checking. This tactic uses a different resolution @@ -445,11 +445,11 @@ Summary of the commands + Use the :cmd:`Typeclasses eauto` command to customize the behavior of this tactic. - :n:`@int_or_var` + :n:`@nat_or_var` Specifies the maximum depth of the search. .. warning:: - The semantics for the limit :n:`@int_or_var` + The semantics for the limit :n:`@nat_or_var` are different than for :tacn:`auto`. By default, if no limit is given, the search is unbounded. Unlike :tacn:`auto`, introduction steps count against the limit, which might result in larger limits being necessary when diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst index f7ce7f1c6c..aa754ab63d 100644 --- a/doc/sphinx/language/extensions/canonical.rst +++ b/doc/sphinx/language/extensions/canonical.rst @@ -490,10 +490,10 @@ We need some infrastructure for that. Definition id {T} {t : T} (x : phantom t) := x. Notation "[find v | t1 ~ t2 ] p" := (fun v (_ : unify t1 t2 None) => p) - (at level 50, v ident, only parsing). + (at level 50, v name, only parsing). Notation "[find v | t1 ~ t2 | s ] p" := (fun v (_ : unify t1 t2 (Some s)) => p) - (at level 50, v ident, only parsing). + (at level 50, v name, only parsing). Notation "'Error : t : s" := (unify _ t (Some s)) (at level 50, format "''Error' : t : s"). diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 6464f085b8..2fc3c9f748 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -480,15 +480,15 @@ separately. They succeed only if there is a success for each goal. For example Do loop ~~~~~~~ -.. tacn:: do @int_or_var @ltac_expr3 +.. tacn:: do @nat_or_var @ltac_expr3 :name: do - The do loop repeats a tactic :token:`int_or_var` times: + The do loop repeats a tactic :token:`nat_or_var` times: - :n:`@ltac_expr` is evaluated to ``v`` which must be a tactic value. This tactic - value ``v`` is applied :token:`int_or_var` times. Supposing :token:`int_or_var` > 1, after the + :n:`@ltac_expr` is evaluated to ``v``, which must be a tactic value. This tactic + value ``v`` is applied :token:`nat_or_var` times. If :token:`nat_or_var` > 1, after the first application of ``v``, ``v`` is applied, at least once, to the generated - subgoals and so on. It fails if the application of ``v`` fails before :token:`int_or_var` + subgoals and so on. It fails if the application of ``v`` fails before :token:`nat_or_var` applications have been completed. :tacn:`do` is an :token:`l3_tactic`. @@ -973,11 +973,11 @@ Timeout We can force a tactic to stop if it has not finished after a certain amount of time: -.. tacn:: timeout @int_or_var @ltac_expr3 +.. tacn:: timeout @nat_or_var @ltac_expr3 :name: timeout :n:`@ltac_expr3` is evaluated to ``v`` which must be a tactic value. The tactic value - ``v`` is applied normally, except that it is interrupted after :n:`@natural` seconds + ``v`` is applied normally, except that it is interrupted after :n:`@nat_or_var` seconds if it is still running. In this case the outcome is a failure. :tacn:`timeout` is an :token:`l3_tactic`. diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index 5283f60b11..9ec568c2c7 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -323,10 +323,12 @@ Performing computations | delta {? @delta_flag } ref_or_pattern_occ ::= @reference {? at @occs_nums } | @one_term {? at @occs_nums } - occs_nums ::= {+ {| @natural | @ident } } - | - {+ {| @natural | @ident } } + occs_nums ::= {+ @nat_or_var } + | - {+ @nat_or_var } int_or_var ::= @integer | @ident + nat_or_var ::= @natural + | @ident unfold_occ ::= @reference {? at @occs_nums } pattern_occ ::= @one_term {? at @occs_nums } diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 5cbd2e400e..df73de846f 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -603,7 +603,7 @@ Here is the basic example of a notation using a binder: .. coqtop:: in Notation "'sigma' x : A , B" := (sigT (fun x : A => B)) - (at level 200, x ident, A at level 200, right associativity). + (at level 200, x name, A at level 200, right associativity). The binding variables in the right-hand side that occur as a parameter of the notation (here :g:`x`) dynamically bind all the occurrences @@ -616,8 +616,9 @@ application of the notation: Check sigma z : nat, z = 0. -Note the :n:`@syntax_modifier x ident` in the declaration of the -notation. It tells to parse :g:`x` as a single identifier. +Note the :n:`@syntax_modifier x name` in the declaration of the +notation. It tells to parse :g:`x` as a single identifier (or as the +unnamed variable :g:`_`). Binders bound in the notation and parsed as patterns ++++++++++++++++++++++++++++++++++++++++++++++++++++ @@ -655,7 +656,7 @@ variable. Here is an example showing the difference: Notation "'subset_bis' ' p , P" := (sig (fun p => P)) (at level 200, p strict pattern). Notation "'subset_bis' p , P " := (sig (fun p => P)) - (at level 200, p ident). + (at level 200, p name). .. coqtop:: all @@ -675,18 +676,19 @@ the following: .. coqdoc:: Notation "{ x : A | P }" := (sig (fun x : A => P)) - (at level 0, x at level 99 as ident). + (at level 0, x at level 99 as name). This is so because the grammar also contains rules starting with :g:`{}` and followed by a term, such as the rule for the notation :g:`{ A } + { B }` for the constant :g:`sumbool` (see :ref:`specification`). -Then, in the rule, ``x ident`` is replaced by ``x at level 99 as ident`` meaning +Then, in the rule, ``x name`` is replaced by ``x at level 99 as name`` meaning that ``x`` is parsed as a term at level 99 (as done in the notation for -:g:`sumbool`), but that this term has actually to be an identifier. +:g:`sumbool`), but that this term has actually to be a name, i.e. an +identifier or :g:`_`. The notation :g:`{ x | P }` is already defined in the standard -library with the ``as ident`` :n:`@syntax_modifier`. We cannot redefine it but +library with the ``as name`` :n:`@syntax_modifier`. We cannot redefine it but one can define an alternative notation, say :g:`{ p such that P }`, using instead ``as pattern``. @@ -702,12 +704,12 @@ Then, the following works: Check {(x,y) such that x+y=0}. To enforce that the pattern should not be used for printing when it -is just an identifier, one could have said +is just a name, one could have said ``p at level 99 as strict pattern``. -Note also that in the absence of a ``as ident``, ``as strict pattern`` or +Note also that in the absence of a ``as name``, ``as strict pattern`` or ``as pattern`` :n:`@syntax_modifier`\s, the default is to consider sub-expressions occurring -in binding position and parsed as terms to be ``as ident``. +in binding position and parsed as terms to be ``as name``. Binders bound in the notation and parsed as general binders +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ @@ -768,7 +770,7 @@ binding position. Here is an example: Definition force n (P:nat -> Prop) := forall n', n' >= n -> P n'. Notation "▢_ n P" := (force n (fun n => P)) - (at level 0, n ident, P at level 9, format "▢_ n P"). + (at level 0, n name, P at level 9, format "▢_ n P"). .. coqtop:: all @@ -946,16 +948,31 @@ position of :g:`x`: (at level 10, f global, a1, an at level 9). In addition to ``global``, one can restrict the syntax of a -sub-expression by using the entry names ``ident`` or ``pattern`` +sub-expression by using the entry names ``ident``, ``name`` or ``pattern`` already seen in :ref:`NotationsWithBinders`, even when the corresponding expression is not used as a binder in the right-hand side. E.g.: + .. todo: these two Set Warnings and the note should be removed when + ident is reactivated with its literal meaning. + +.. coqtop:: none + + Set Warnings "-deprecated-ident-entry". + .. coqtop:: in Notation "'apply_id' f a1 .. an" := (.. (f a1) .. an) (at level 10, f ident, a1, an at level 9). +.. coqtop:: none + + Set Warnings "+deprecated-ident-entry". + +.. note:: As of version 8.13, the entry ``ident`` is a deprecated + alias for ``name``. In the future, it is planned to strictly + parse an identifier (excluding :g:`_`). + .. _custom-entries: Custom entries @@ -1113,6 +1130,31 @@ 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. +Another special situation is when parsing global references or +identifiers. To indicate that a custom entry should parse identifiers, +use the following form: + +.. coqtop:: none + + Reset Initial. + Declare Custom Entry expr. + +.. coqtop:: in + + Notation "x" := x (in custom expr at level 0, x ident). + +Similarly, to indicate that a custom entry should parse global references +(i.e. qualified or non qualified identifiers), use the following form: + +.. coqtop:: none + + Reset Initial. + Declare Custom Entry expr. + +.. coqtop:: in + + Notation "x" := x (in custom expr at level 0, x global). + .. cmd:: Print Custom Grammar @ident :name: Print Custom Grammar @@ -1142,6 +1184,7 @@ Here are the syntax elements used by the various notation commands. | only printing | format @string {? @string } explicit_subentry ::= ident + | name | global | bigint | strict pattern {? at level @natural } @@ -1151,6 +1194,7 @@ Here are the syntax elements used by the various notation commands. | custom @ident {? at @level } {? @binder_interp } | pattern {? at level @natural } binder_interp ::= as ident + | as name | as pattern | as strict pattern level ::= level @natural @@ -1188,6 +1232,27 @@ Here are the syntax elements used by the various notation commands. due to legacy notation in the Coq standard library. It can be turned on with the ``-w disj-pattern-notation`` flag. +.. note:: + + As of version 8.13, the entry ``ident`` is a deprecated alias for + ``name``. In the future, it is planned to strictly parse an + identifier (to the exclusion of :g:`_`). If the intent was to use + ``ident`` as an identifier (excluding :g:`_`), just silence the warning with + :n:`Set Warnings "-deprecated-ident-entry"` and it should automatically + get its intended meaning in version 8.15. + + Similarly, ``as ident`` is a deprecated alias for ``as name``, which + will only accept an identifier in the future. If the + intent was to use ``as ident`` as an identifier + (excluding :g:`_`), just silence the warning with + :n:`Set Warnings "-deprecated-as-ident-kind"`. + + However, this deprecation does not apply to custom entries, where it + already denotes an identifier, as expected. + + .. todo: the note above should be removed at the end of deprecation + phase of ident + .. .. _Scopes: Notation scopes diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 816acba4c1..4080eaae08 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -815,7 +815,10 @@ ltac_expr3: [ | REPLACE "abstract" ltac_expr2 "using" ident | WITH "abstract" ltac_expr2 OPT ( "using" ident ) | l3_tactic -| EDIT "do" ADD_OPT int_or_var ssrmmod ssrdotac ssrclauses TAG SSR +(* | EDIT "do" ADD_OPT nat_or_var ssrmmod ssrdotac ssrclauses TAG SSR *) +| DELETE "do" ssrmmod ssrdotac ssrclauses (* SSR plugin *) +| DELETE "do" ssrortacarg ssrclauses (* SSR plugin *) +| DELETE "do" nat_or_var ssrmmod ssrdotac ssrclauses (* SSR plugin *) | MOVEALLBUT ltac_builtins | l3_tactic | ltac_expr2 @@ -917,13 +920,13 @@ simple_tactic: [ | REPLACE "cofix" ident "with" LIST1 cofixdecl | WITH "cofix" ident OPT ( "with" LIST1 cofixdecl ) | DELETE "constructor" -| DELETE "constructor" int_or_var -| REPLACE "constructor" int_or_var "with" bindings -| WITH "constructor" OPT int_or_var OPT ( "with" bindings ) +| DELETE "constructor" nat_or_var +| REPLACE "constructor" nat_or_var "with" bindings +| WITH "constructor" OPT nat_or_var OPT ( "with" bindings ) | DELETE "econstructor" -| DELETE "econstructor" int_or_var -| REPLACE "econstructor" int_or_var "with" bindings -| WITH "econstructor" OPT ( int_or_var OPT ( "with" bindings ) ) +| DELETE "econstructor" nat_or_var +| REPLACE "econstructor" nat_or_var "with" bindings +| WITH "econstructor" OPT ( nat_or_var OPT ( "with" bindings ) ) | DELETE "dependent" "rewrite" orient constr | REPLACE "dependent" "rewrite" orient constr "in" hyp | WITH "dependent" "rewrite" orient constr OPT ( "in" hyp ) @@ -1042,12 +1045,12 @@ simple_tactic: [ | DELETE "finish_timing" OPT string | REPLACE "finish_timing" "(" string ")" OPT string | WITH "finish_timing" OPT ( "(" string ")" ) OPT string -| REPLACE "hresolve_core" "(" ident ":=" constr ")" "at" int_or_var "in" constr -| WITH "hresolve_core" "(" ident ":=" constr ")" OPT ( "at" int_or_var ) "in" constr +| REPLACE "hresolve_core" "(" ident ":=" constr ")" "at" nat_or_var "in" constr +| WITH "hresolve_core" "(" ident ":=" constr ")" OPT ( "at" nat_or_var ) "in" constr | DELETE "hresolve_core" "(" ident ":=" constr ")" "in" constr -| EDIT "psatz_R" ADD_OPT int_or_var tactic -| EDIT "psatz_Q" ADD_OPT int_or_var tactic -| EDIT "psatz_Z" ADD_OPT int_or_var tactic +| EDIT "psatz_R" ADD_OPT nat_or_var tactic +| EDIT "psatz_Q" ADD_OPT nat_or_var tactic +| EDIT "psatz_Z" ADD_OPT nat_or_var tactic | REPLACE "subst" LIST1 hyp | WITH "subst" LIST0 hyp | DELETE "subst" @@ -1064,11 +1067,11 @@ simple_tactic: [ | DELETE "transparent_abstract" tactic3 | REPLACE "transparent_abstract" tactic3 "using" ident | WITH "transparent_abstract" ltac_expr3 OPT ( "using" ident ) -| "typeclasses" "eauto" OPT "bfs" OPT int_or_var OPT ( "with" LIST1 preident ) -| DELETE "typeclasses" "eauto" "bfs" OPT int_or_var "with" LIST1 preident -| DELETE "typeclasses" "eauto" OPT int_or_var "with" LIST1 preident -| DELETE "typeclasses" "eauto" "bfs" OPT int_or_var -| DELETE "typeclasses" "eauto" OPT int_or_var +| "typeclasses" "eauto" OPT "bfs" OPT nat_or_var OPT ( "with" LIST1 preident ) +| DELETE "typeclasses" "eauto" "bfs" OPT nat_or_var "with" LIST1 preident +| DELETE "typeclasses" "eauto" OPT nat_or_var "with" LIST1 preident +| DELETE "typeclasses" "eauto" "bfs" OPT nat_or_var +| DELETE "typeclasses" "eauto" OPT nat_or_var (* in Tactic Notation: *) | "setoid_replace" constr "with" constr OPT ( "using" "relation" constr ) OPT ( "in" hyp ) OPT ( "at" LIST1 int_or_var ) OPT ( "by" ltac_expr3 ) @@ -1789,7 +1792,7 @@ tactic_notation_tactics: [ | "field_simplify_eq" OPT ( "[" LIST1 constr "]" ) OPT ( "in" ident ) | "intuition" OPT ltac_expr5 (* todo: Not too keen on things like "with_power_flags" in tauto.ml, not easy to follow *) | "nsatz" OPT ( "with" "radicalmax" ":=" constr "strategy" ":=" constr "parameters" ":=" constr "variables" ":=" constr ) -| "psatz" constr OPT int_or_var +| "psatz" constr OPT nat_or_var | "ring" OPT ( "[" LIST1 constr "]" ) | "ring_simplify" OPT ( "[" LIST1 constr "]" ) LIST1 constr OPT ( "in" ident ) (* todo: ident was "hyp", worth keeping? *) ] @@ -2536,7 +2539,6 @@ SPLICE: [ | by_arg_tac | by_tactic | quantified_hypothesis -| nat_or_var | in_hyp_list | rename | export_token diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 03a20d621b..d01f66c6d7 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1420,6 +1420,7 @@ syntax_modifiers: [ explicit_subentry: [ | "ident" +| "name" | "global" | "bigint" | "binder" @@ -1440,6 +1441,7 @@ at_level_opt: [ binder_interp: [ | "as" "ident" +| "as" "name" | "as" "pattern" | "as" "strict" "pattern" ] @@ -1479,11 +1481,11 @@ simple_tactic: [ | "right" "with" bindings | "eright" "with" bindings | "constructor" -| "constructor" int_or_var -| "constructor" int_or_var "with" bindings +| "constructor" nat_or_var +| "constructor" nat_or_var "with" bindings | "econstructor" -| "econstructor" int_or_var -| "econstructor" int_or_var "with" bindings +| "econstructor" nat_or_var +| "econstructor" nat_or_var "with" bindings | "specialize" constr_with_bindings | "specialize" constr_with_bindings "as" simple_intropattern | "symmetry" @@ -1582,9 +1584,9 @@ simple_tactic: [ | "generalize_eqs_vars" hyp | "dependent" "generalize_eqs_vars" hyp | "specialize_eqs" hyp -| "hresolve_core" "(" ident ":=" constr ")" "at" int_or_var "in" constr +| "hresolve_core" "(" ident ":=" constr ")" "at" nat_or_var "in" constr | "hresolve_core" "(" ident ":=" constr ")" "in" constr -| "hget_evar" int_or_var +| "hget_evar" nat_or_var | "destauto" | "destauto" "in" hyp | "transparent_abstract" tactic3 @@ -1617,25 +1619,25 @@ simple_tactic: [ | "trivial" auto_using hintbases | "info_trivial" auto_using hintbases | "debug" "trivial" auto_using hintbases -| "auto" OPT int_or_var auto_using hintbases -| "info_auto" OPT int_or_var auto_using hintbases -| "debug" "auto" OPT int_or_var auto_using hintbases -| "eauto" OPT int_or_var OPT int_or_var auto_using hintbases -| "new" "auto" OPT int_or_var auto_using hintbases -| "debug" "eauto" OPT int_or_var OPT int_or_var auto_using hintbases -| "info_eauto" OPT int_or_var OPT int_or_var auto_using hintbases -| "dfs" "eauto" OPT int_or_var auto_using hintbases -| "bfs" "eauto" OPT int_or_var auto_using hintbases +| "auto" OPT nat_or_var auto_using hintbases +| "info_auto" OPT nat_or_var auto_using hintbases +| "debug" "auto" OPT nat_or_var auto_using hintbases +| "eauto" OPT nat_or_var OPT nat_or_var auto_using hintbases +| "new" "auto" OPT nat_or_var auto_using hintbases +| "debug" "eauto" OPT nat_or_var OPT nat_or_var auto_using hintbases +| "info_eauto" OPT nat_or_var OPT nat_or_var auto_using hintbases +| "dfs" "eauto" OPT nat_or_var auto_using hintbases +| "bfs" "eauto" OPT nat_or_var auto_using hintbases | "autounfold" hintbases clause_dft_concl | "autounfold_one" hintbases "in" hyp | "autounfold_one" hintbases | "unify" constr constr | "unify" constr constr "with" preident | "convert_concl_no_check" constr -| "typeclasses" "eauto" "bfs" OPT int_or_var "with" LIST1 preident -| "typeclasses" "eauto" OPT int_or_var "with" LIST1 preident -| "typeclasses" "eauto" "bfs" OPT int_or_var -| "typeclasses" "eauto" OPT int_or_var +| "typeclasses" "eauto" "bfs" OPT nat_or_var "with" LIST1 preident +| "typeclasses" "eauto" OPT nat_or_var "with" LIST1 preident +| "typeclasses" "eauto" "bfs" OPT nat_or_var +| "typeclasses" "eauto" OPT nat_or_var | "head_of_constr" ident constr | "not_evar" constr | "is_ground" constr @@ -1734,7 +1736,7 @@ simple_tactic: [ | "restart_timer" OPT string | "finish_timing" OPT string | "finish_timing" "(" string ")" OPT string -| "psatz_Z" int_or_var tactic (* micromega plugin *) +| "psatz_Z" nat_or_var tactic (* micromega plugin *) | "psatz_Z" tactic (* micromega plugin *) | "xlia" tactic (* micromega plugin *) | "xnlia" tactic (* micromega plugin *) @@ -1745,9 +1747,9 @@ simple_tactic: [ | "sos_R" tactic (* micromega plugin *) | "lra_Q" tactic (* micromega plugin *) | "lra_R" tactic (* micromega plugin *) -| "psatz_R" int_or_var tactic (* micromega plugin *) +| "psatz_R" nat_or_var tactic (* micromega plugin *) | "psatz_R" tactic (* micromega plugin *) -| "psatz_Q" int_or_var tactic (* micromega plugin *) +| "psatz_Q" nat_or_var tactic (* micromega plugin *) | "psatz_Q" tactic (* micromega plugin *) | "zify_iter_specs" (* micromega plugin *) | "zify_op" (* micromega plugin *) @@ -2022,8 +2024,8 @@ ltac_expr4: [ ltac_expr3: [ | "try" ltac_expr3 -| "do" int_or_var ltac_expr3 -| "timeout" int_or_var ltac_expr3 +| "do" nat_or_var ltac_expr3 +| "timeout" nat_or_var ltac_expr3 | "time" OPT string ltac_expr3 | "repeat" ltac_expr3 | "progress" ltac_expr3 @@ -2036,7 +2038,7 @@ ltac_expr3: [ | ltac_expr2 | "do" ssrmmod ssrdotac ssrclauses (* SSR plugin *) | "do" ssrortacarg ssrclauses (* SSR plugin *) -| "do" int_or_var ssrmmod ssrdotac ssrclauses (* SSR plugin *) +| "do" nat_or_var ssrmmod ssrdotac ssrclauses (* SSR plugin *) | "abstract" ssrdgens (* SSR plugin *) ] diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index 0209cf762a..f62dd8f731 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -652,8 +652,8 @@ ref_or_pattern_occ: [ ] occs_nums: [ -| LIST1 [ natural | ident ] -| "-" LIST1 [ natural | ident ] +| LIST1 nat_or_var +| "-" LIST1 nat_or_var ] int_or_var: [ @@ -661,6 +661,11 @@ int_or_var: [ | ident ] +nat_or_var: [ +| natural +| ident +] + unfold_occ: [ | reference OPT ( "at" occs_nums ) ] @@ -1574,6 +1579,7 @@ syntax_modifier: [ explicit_subentry: [ | "ident" +| "name" | "global" | "bigint" | "strict" "pattern" OPT ( "at" "level" natural ) @@ -1586,6 +1592,7 @@ explicit_subentry: [ binder_interp: [ | "as" "ident" +| "as" "name" | "as" "pattern" | "as" "strict" "pattern" ] @@ -1620,8 +1627,8 @@ simple_tactic: [ | "eleft" OPT ( "with" bindings ) | "right" OPT ( "with" bindings ) | "eright" OPT ( "with" bindings ) -| "constructor" OPT int_or_var OPT ( "with" bindings ) -| "econstructor" OPT ( int_or_var OPT ( "with" bindings ) ) +| "constructor" OPT nat_or_var OPT ( "with" bindings ) +| "econstructor" OPT ( nat_or_var OPT ( "with" bindings ) ) | "specialize" one_term OPT ( "with" bindings ) OPT ( "as" simple_intropattern ) | "symmetry" OPT ( "in" in_clause ) | "split" OPT ( "with" bindings ) @@ -1648,8 +1655,8 @@ simple_tactic: [ | bullet | "}" | "try" ltac_expr3 -| "do" int_or_var ltac_expr3 -| "timeout" int_or_var ltac_expr3 +| "do" nat_or_var ltac_expr3 +| "timeout" nat_or_var ltac_expr3 | "time" OPT string ltac_expr3 | "repeat" ltac_expr3 | "progress" ltac_expr3 @@ -1658,8 +1665,6 @@ simple_tactic: [ | "infoH" ltac_expr3 | "abstract" ltac_expr2 OPT ( "using" ident ) | "only" selector ":" ltac_expr3 -| "do" "[" ssrortacs "]" OPT ssr_in (* SSR plugin *) -| "do" OPT int_or_var ssrmmod [ ltac_expr3 | "[" ssrortacs "]" (* SSR plugin *) ] OPT ssr_in (* SSR plugin *) | "tryif" ltac_expr "then" ltac_expr "else" ltac_expr2 | "first" "[" LIST0 ltac_expr SEP "|" "]" | "solve" "[" LIST0 ltac_expr SEP "|" "]" @@ -1718,8 +1723,8 @@ simple_tactic: [ | "generalize_eqs_vars" ident | "dependent" "generalize_eqs_vars" ident | "specialize_eqs" ident -| "hresolve_core" "(" ident ":=" one_term ")" OPT ( "at" int_or_var ) "in" one_term -| "hget_evar" int_or_var +| "hresolve_core" "(" ident ":=" one_term ")" OPT ( "at" nat_or_var ) "in" one_term +| "hget_evar" nat_or_var | "destauto" OPT ( "in" ident ) | "transparent_abstract" ltac_expr3 OPT ( "using" ident ) | "constr_eq" one_term one_term @@ -1756,20 +1761,20 @@ simple_tactic: [ | "trivial" OPT auto_using OPT hintbases | "info_trivial" OPT auto_using OPT hintbases | "debug" "trivial" OPT auto_using OPT hintbases -| "auto" OPT int_or_var OPT auto_using OPT hintbases -| "info_auto" OPT int_or_var OPT auto_using OPT hintbases -| "debug" "auto" OPT int_or_var OPT auto_using OPT hintbases -| "eauto" OPT int_or_var OPT int_or_var OPT auto_using OPT hintbases -| "new" "auto" OPT int_or_var OPT auto_using OPT hintbases -| "debug" "eauto" OPT int_or_var OPT int_or_var OPT auto_using OPT hintbases -| "info_eauto" OPT int_or_var OPT int_or_var OPT auto_using OPT hintbases -| "dfs" "eauto" OPT int_or_var OPT auto_using OPT hintbases -| "bfs" "eauto" OPT int_or_var OPT auto_using OPT hintbases +| "auto" OPT nat_or_var OPT auto_using OPT hintbases +| "info_auto" OPT nat_or_var OPT auto_using OPT hintbases +| "debug" "auto" OPT nat_or_var OPT auto_using OPT hintbases +| "eauto" OPT nat_or_var OPT nat_or_var OPT auto_using OPT hintbases +| "new" "auto" OPT nat_or_var OPT auto_using OPT hintbases +| "debug" "eauto" OPT nat_or_var OPT nat_or_var OPT auto_using OPT hintbases +| "info_eauto" OPT nat_or_var OPT nat_or_var OPT auto_using OPT hintbases +| "dfs" "eauto" OPT nat_or_var OPT auto_using OPT hintbases +| "bfs" "eauto" OPT nat_or_var OPT auto_using OPT hintbases | "autounfold" OPT hintbases OPT clause_dft_concl | "autounfold_one" OPT hintbases OPT ( "in" ident ) | "unify" one_term one_term OPT ( "with" ident ) | "convert_concl_no_check" one_term -| "typeclasses" "eauto" OPT "bfs" OPT int_or_var OPT ( "with" LIST1 ident ) +| "typeclasses" "eauto" OPT "bfs" OPT nat_or_var OPT ( "with" LIST1 ident ) | "head_of_constr" ident one_term | "not_evar" one_term | "is_ground" one_term @@ -1859,7 +1864,7 @@ simple_tactic: [ | "functional" "inversion" [ ident | natural ] OPT qualid (* funind plugin *) | "functional" "induction" term OPT ( "using" one_term OPT ( "with" bindings ) ) OPT ( "as" simple_intropattern ) (* funind plugin *) | "soft" "functional" "induction" LIST1 one_term OPT ( "using" one_term OPT ( "with" bindings ) ) OPT ( "as" simple_intropattern ) (* funind plugin *) -| "psatz_Z" OPT int_or_var ltac_expr +| "psatz_Z" OPT nat_or_var ltac_expr | "xlia" ltac_expr (* micromega plugin *) | "xnlia" ltac_expr (* micromega plugin *) | "xnra" ltac_expr (* micromega plugin *) @@ -1869,8 +1874,8 @@ simple_tactic: [ | "sos_R" ltac_expr (* micromega plugin *) | "lra_Q" ltac_expr (* micromega plugin *) | "lra_R" ltac_expr (* micromega plugin *) -| "psatz_R" OPT int_or_var ltac_expr -| "psatz_Q" OPT int_or_var ltac_expr +| "psatz_R" OPT nat_or_var ltac_expr +| "psatz_Q" OPT nat_or_var ltac_expr | "zify_iter_specs" (* micromega plugin *) | "zify_op" (* micromega plugin *) | "zify_saturate" (* micromega plugin *) @@ -1942,7 +1947,7 @@ simple_tactic: [ | "field_simplify_eq" OPT ( "[" LIST1 one_term "]" ) OPT ( "in" ident ) | "intuition" OPT ltac_expr | "nsatz" OPT ( "with" "radicalmax" ":=" one_term "strategy" ":=" one_term "parameters" ":=" one_term "variables" ":=" one_term ) -| "psatz" one_term OPT int_or_var +| "psatz" one_term OPT nat_or_var | "ring" OPT ( "[" LIST1 one_term "]" ) | "ring_simplify" OPT ( "[" LIST1 one_term "]" ) LIST1 one_term OPT ( "in" ident ) | "match" ltac2_expr5 "with" OPT ltac2_branches "end" |