diff options
Diffstat (limited to 'doc')
10 files changed, 76 insertions, 12 deletions
diff --git a/doc/changelog/03-notations/12965-master+fix9569-propagage-binding-vars-notations.rst b/doc/changelog/03-notations/12965-master+fix9569-propagage-binding-vars-notations.rst new file mode 100644 index 0000000000..e63ab9696e --- /dev/null +++ b/doc/changelog/03-notations/12965-master+fix9569-propagage-binding-vars-notations.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Capture of the name of global references by + binders in the presence of notations for binders + (`#12965 <https://github.com/coq/coq/pull/12965>`_, + fixes `#9569 <https://github.com/coq/coq/issues/9569>`_, + by Hugo Herbelin). diff --git a/doc/changelog/03-notations/13265-master+allow-single-binder-entry.rst b/doc/changelog/03-notations/13265-master+allow-single-binder-entry.rst new file mode 100644 index 0000000000..c973e157dd --- /dev/null +++ b/doc/changelog/03-notations/13265-master+allow-single-binder-entry.rst @@ -0,0 +1,6 @@ +- **Added:** + The :n:`@binder` entry of :cmd:`Notation` can now be used in + notations expecting a single (non-recursive) binder + (`#13265 <https://github.com/coq/coq/pull/13265>`_, + by Hugo Herbelin, see section :n:`notations-and-binders` of the + reference manual). diff --git a/doc/changelog/04-tactics/13237-master+fix13235-no-degenerate-in-hyps-clause.rst b/doc/changelog/04-tactics/13237-master+fix13235-no-degenerate-in-hyps-clause.rst new file mode 100644 index 0000000000..bc67fd025a --- /dev/null +++ b/doc/changelog/04-tactics/13237-master+fix13235-no-degenerate-in-hyps-clause.rst @@ -0,0 +1,6 @@ +- **Changed:** + Giving an empty list of occurrences after :n:`in` in tactics is no + longer permitted. Omitting the :n:`in` gives the same behavior + (`#13237 <https://github.com/coq/coq/pull/13236>`_, + fixes `#13235 <https://github.com/coq/coq/issues/13235>`_, + by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/13403-occs_nums_nat.rst b/doc/changelog/04-tactics/13403-occs_nums_nat.rst new file mode 100644 index 0000000000..5dfa90a267 --- /dev/null +++ b/doc/changelog/04-tactics/13403-occs_nums_nat.rst @@ -0,0 +1,7 @@ +- **Removed:** + :n:`at @occs_nums` clauses in tactics such as tacn:`unfold` + no longer allow negative values. A "-" before the + list (for set complement) is still supported. Ex: "at -1 -2" + is no longer supported but "at -1 2" is. + (`#13403 <https://github.com/coq/coq/pull/13403>`_, + by Jim Fehrle). diff --git a/doc/changelog/07-commands-and-options/13352-cep-48.rst b/doc/changelog/07-commands-and-options/13352-cep-48.rst new file mode 100644 index 0000000000..cb2eeea74b --- /dev/null +++ b/doc/changelog/07-commands-and-options/13352-cep-48.rst @@ -0,0 +1,12 @@ +- **Changed:** + Option -native-compiler of the configure script now impacts the + default value of the option -native-compiler of coqc. The + -native-compiler option of the configure script is added an ondemand + value, which becomes the default, thus preserving the previous default + behavior. + The stdlib is still precompiled when configuring with -native-compiler + yes. It is not precompiled otherwise. + This an implementation of point 2 of + `CEP #48 <https://github.com/coq/ceps/pull/48>`_ + (`#13352 <https://github.com/coq/coq/pull/13352>`_, + by Pierre Roux). diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index f3f69a2fdc..5283f60b11 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -274,9 +274,13 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. .. exn:: Too few occurrences. :undocumented: - .. tacv:: change @term {? {? at {+ @natural}} with @term} in @ident + .. tacv:: change @term {? {? at {+ @natural}} with @term} in @goal_occurrences - This applies the :tacn:`change` tactic not to the goal but to the hypothesis :n:`@ident`. + In the presence of :n:`with`, this applies :tacn:`change` to the + occurrences specified by :n:`@goal_occurrences`. In the + absence of :n:`with`, :n:`@goal_occurrences` is expected to + only list hypotheses (and optionally the conclusion) without + specifying occurrences (i.e. no :n:`at` clause). .. tacv:: now_show @term @@ -320,7 +324,7 @@ Performing computations ref_or_pattern_occ ::= @reference {? at @occs_nums } | @one_term {? at @occs_nums } occs_nums ::= {+ {| @natural | @ident } } - | - {| @natural | @ident } {* @int_or_var } + | - {+ {| @natural | @ident } } int_or_var ::= @integer | @ident unfold_occ ::= @reference {? at @occs_nums } diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 16c8586a9f..5cbd2e400e 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -709,6 +709,30 @@ Note also that in the absence of a ``as ident``, ``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``. +Binders bound in the notation and parsed as general binders ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ + +It is also possible to rely on Coq's syntax of binders using the +`binder` modifier as follows: + +.. coqtop:: in + + Notation "'myforall' p , [ P , Q ] " := (forall p, P -> Q) + (at level 200, p binder). + +In this case, all of :n:`@ident`, :n:`{@ident}`, :n:`[@ident]`, :n:`@ident:@type`, +:n:`{@ident:@type}`, :n:`[@ident:@type]`, :n:`'@pattern` can be used in place of +the corresponding notation variable. In particular, the binder can +declare implicit arguments: + +.. coqtop:: all + + Check fun (f : myforall {a}, [a=0, Prop]) => f eq_refl. + Check myforall '((x,y):nat*nat), [ x = y, True ]. + +By using instead `closed binder`, the same list of binders is allowed +except that :n:`@ident:@type` requires parentheses around. + .. _NotationsWithBinders: Binders not bound in the notation diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 4c1956d172..816acba4c1 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1939,11 +1939,6 @@ tac2rec_fields: [ | LIST1 tac2rec_field SEP ";" OPT ";" TAG Ltac2 ] -(* todo: weird productions, ints only after an initial "-"??: - occs_nums: [ - | LIST1 [ natural | ident ] - | "-" [ natural | ident ] LIST0 int_or_var -*) ltac2_occs_nums: [ | DELETE LIST1 nat_or_anti (* Ltac2 plugin *) | REPLACE "-" nat_or_anti LIST0 nat_or_anti (* Ltac2 plugin *) diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index b5d57f92e9..03a20d621b 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -480,6 +480,7 @@ opt_hintbases: [ command: [ | "Goal" lconstr | "Proof" +| "Proof" "using" G_vernac.section_subset_expr | "Proof" "Mode" string | "Proof" lconstr | "Abort" @@ -604,7 +605,7 @@ command: [ | "Typeclasses" "Opaque" LIST1 reference | "Typeclasses" "eauto" ":=" debug eauto_search_strategy OPT natural | "Proof" "with" Pltac.tactic OPT [ "using" G_vernac.section_subset_expr ] -| "Proof" "using" G_vernac.section_subset_expr OPT [ "with" Pltac.tactic ] +| "Proof" "using" G_vernac.section_subset_expr "with" Pltac.tactic | "Tactic" "Notation" OPT ltac_tactic_level LIST1 ltac_production_item ":=" tactic | "Print" "Ltac" reference | "Locate" "Ltac" reference @@ -2328,7 +2329,7 @@ conversion: [ occs_nums: [ | LIST1 nat_or_var -| "-" nat_or_var LIST0 int_or_var +| "-" LIST1 nat_or_var ] occs: [ @@ -2538,6 +2539,7 @@ or_and_intropattern_loc: [ as_or_and_ipat: [ | "as" or_and_intropattern_loc +| "as" equality_intropattern | ] diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index c9d70a88fc..0209cf762a 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -653,7 +653,7 @@ ref_or_pattern_occ: [ occs_nums: [ | LIST1 [ natural | ident ] -| "-" [ natural | ident ] LIST0 int_or_var +| "-" LIST1 [ natural | ident ] ] int_or_var: [ @@ -953,6 +953,7 @@ command: [ | "Extract" "Inductive" qualid "=>" [ ident | string ] "[" LIST0 [ ident | string ] "]" OPT string (* extraction plugin *) | "Show" "Extraction" (* extraction plugin *) | "Proof" +| "Proof" "using" section_var_expr | "Proof" "Mode" string | "Proof" term | "Abort" OPT [ "All" | ident ] @@ -1033,7 +1034,7 @@ command: [ | "Typeclasses" "Opaque" LIST1 qualid | "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" [ "bfs" | "dfs" ] ")" ) OPT natural | "Proof" "with" ltac_expr OPT [ "using" section_var_expr ] -| "Proof" "using" section_var_expr OPT [ "with" ltac_expr ] +| "Proof" "using" section_var_expr "with" ltac_expr | "Tactic" "Notation" OPT ( "(" "at" "level" natural ")" ) LIST1 ltac_production_item ":=" ltac_expr | "Print" "Rewrite" "HintDb" ident | "Print" "Ltac" qualid @@ -1969,6 +1970,7 @@ or_and_intropattern_loc: [ as_or_and_ipat: [ | "as" or_and_intropattern_loc +| "as" equality_intropattern ] eqn_ipat: [ |