aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
Diffstat (limited to 'doc')
-rw-r--r--doc/changelog/01-kernel/13356-primarray-cumul.rst5
-rw-r--r--doc/changelog/07-commands-and-options/13339-proof-using-noinit.rst5
-rw-r--r--doc/sphinx/addendum/type-classes.rst13
-rw-r--r--doc/sphinx/language/core/definitions.rst21
-rw-r--r--doc/sphinx/language/extensions/match.rst7
-rw-r--r--doc/sphinx/proof-engine/vernacular-commands.rst20
-rw-r--r--doc/tools/docgram/common.edit_mlg7
-rw-r--r--doc/tools/docgram/orderedGrammar28
8 files changed, 70 insertions, 36 deletions
diff --git a/doc/changelog/01-kernel/13356-primarray-cumul.rst b/doc/changelog/01-kernel/13356-primarray-cumul.rst
new file mode 100644
index 0000000000..978ca325bf
--- /dev/null
+++ b/doc/changelog/01-kernel/13356-primarray-cumul.rst
@@ -0,0 +1,5 @@
+- **Changed:** Primitive arrays are now irrelevant in their single
+ polymorphic universe (same as a polymorphic cumulative list
+ inductive would be) (`#13356
+ <https://github.com/coq/coq/pull/13356>`_, fixes `#13354
+ <https://github.com/coq/coq/issues/13354>`_, by Gaëtan Gilbert).
diff --git a/doc/changelog/07-commands-and-options/13339-proof-using-noinit.rst b/doc/changelog/07-commands-and-options/13339-proof-using-noinit.rst
new file mode 100644
index 0000000000..9ae759be56
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/13339-proof-using-noinit.rst
@@ -0,0 +1,5 @@
+- **Added:**
+ The :cmd:`Proof using` command can now be used without loading the
+ Ltac plugin (`-noinit` mode)
+ (`#13339 <https://github.com/coq/coq/pull/13339>`_,
+ by Théo Zimmermann).
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst
index cdd31fcb86..56d90b33d8 100644
--- a/doc/sphinx/addendum/type-classes.rst
+++ b/doc/sphinx/addendum/type-classes.rst
@@ -336,20 +336,23 @@ Summary of the commands
.. cmd:: Instance {? @ident_decl {* @binder } } : @type {? @hint_info } {? {| := %{ {* @field_def } %} | := @term } }
- .. insertprodn hint_info hint_info
+ .. insertprodn hint_info one_pattern
.. prodn::
- hint_info ::= %| {? @natural } {? @one_term }
+ hint_info ::= %| {? @natural } {? @one_pattern }
+ one_pattern ::= @one_term
Declares a typeclass instance named
:token:`ident_decl` of the class :n:`@type` with the specified parameters and with
fields defined by :token:`field_def`, where each field must be a declared field of
the class.
- Add one or more :token:`binder`\s to declare a parameterized instance. :token:`hint_info`
- specifies the hint priority, where 0 is the highest priority as for
+ Adds one or more :token:`binder`\s to declare a parameterized instance. :token:`hint_info`
+ may be used to specify the hint priority, where 0 is the highest priority as for
:tacn:`auto` hints. If the priority is not specified, the default is the number
- of non-dependent binders of the instance.
+ of non-dependent binders of the instance. If :token:`one_pattern` is given, terms
+ matching that pattern will trigger use of the instance. Otherwise,
+ use is triggered based on the conclusion of the type.
This command supports the :attr:`global` attribute that can be
used on instances declared in a section so that their
diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst
index 4ea3ea5e6d..79489c85f6 100644
--- a/doc/sphinx/language/core/definitions.rst
+++ b/doc/sphinx/language/core/definitions.rst
@@ -13,15 +13,18 @@ Let-in definitions
.. prodn::
term_let ::= let @name {? : @type } := @term in @term
| let @name {+ @binder } {? : @type } := @term in @term
- | let ( {*, @name } ) {? {? as @name } return @term100 } := @term in @term
- | let ' @pattern := @term {? return @term100 } in @term
- | let ' @pattern in @pattern := @term return @term100 in @term
-
-:n:`let @ident := @term in @term’`
-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’`.
+ | @destructuring_let
+
+:n:`let @ident := @term__1 in @term__2` represents the local binding of
+the variable :n:`@ident` to the value :n:`@term__1` in :n:`@term__2`.
+
+:n:`let @ident {+ @binder} := @term__1 in @term__2` is an abbreviation
+for :n:`let @ident := fun {+ @binder} => @term__1 in @term__2`.
+
+.. seealso::
+
+ Extensions of the `let ... in ...` syntax are described in
+ :ref:`irrefutable-patterns`.
.. index::
single: ... : ... (type cast)
diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst
index 23389eba3b..8e62c2af13 100644
--- a/doc/sphinx/language/extensions/match.rst
+++ b/doc/sphinx/language/extensions/match.rst
@@ -86,6 +86,13 @@ Pattern-matching on terms inhabiting inductive type having only one
constructor can be alternatively written using :g:`let … in …`
constructions. There are two variants of them.
+.. insertprodn destructuring_let destructuring_let
+
+.. prodn::
+ destructuring_let ::= let ( {*, @name } ) {? {? as @name } return @term100 } := @term in @term
+ | let ' @pattern := @term {? return @term100 } in @term
+ | let ' @pattern in @pattern := @term return @term100 in @term
+
First destructuring let syntax
++++++++++++++++++++++++++++++
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 7baf193266..86d1d25745 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -133,7 +133,7 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`).
.. prodn::
search_item ::= {? {| head | hyp | concl | headhyp | headconcl } : } @string {? % @scope_key }
- | {? {| head | hyp | concl | headhyp | headconcl } : } @one_term
+ | {? {| head | hyp | concl | headhyp | headconcl } : } @one_pattern
| is : @logical_kind
Searched objects can be filtered by patterns, by the constants they
@@ -141,9 +141,9 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`).
names.
The location of the pattern or constant within a term
- :n:`@one_term`
+ :n:`@one_pattern`
Search for objects whose type contains a subterm matching the
- pattern :n:`@one_term`. Holes of the pattern are indicated by
+ pattern :n:`@one_pattern`. Holes of the pattern are indicated by
`_` or :n:`?@ident`. If the same :n:`?@ident` occurs more than
once in the pattern, all occurrences in the subterm must be
identical. See :ref:`this example <search-pattern>`.
@@ -312,7 +312,7 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`).
Search is:Instance [ Reflexive | Symmetric ].
-.. cmd:: SearchHead @one_term {? {| inside | outside } {+ @qualid } }
+.. cmd:: SearchHead @one_pattern {? {| inside | outside } {+ @qualid } }
.. deprecated:: 8.12
@@ -320,8 +320,8 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`).
Displays the name and type of all hypotheses of the
selected goal (if any) and theorems of the current context that have the
- form :n:`{? forall {* @binder }, } {* P__i -> } C` where :n:`@one_term`
- matches a subterm of `C` in head position. For example, a :n:`@one_term` of `f _ b`
+ form :n:`{? forall {* @binder }, } {* P__i -> } C` where :n:`@one_pattern`
+ matches a subterm of `C` in head position. For example, a :n:`@one_pattern` of `f _ b`
matches `f a b`, which is a subterm of `C` in head position when `C` is `f a b c`.
See :cmd:`Search` for an explanation of the `inside`/`outside` clauses.
@@ -337,12 +337,12 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`).
SearchHead le.
SearchHead (@eq bool).
-.. cmd:: SearchPattern @one_term {? {| inside | outside } {+ @qualid } }
+.. cmd:: SearchPattern @one_pattern {? {| inside | outside } {+ @qualid } }
Displays the name and type of all hypotheses of the
selected goal (if any) and theorems of the current context
ending with :n:`{? forall {* @binder }, } {* P__i -> } C` that match the pattern
- :n:`@one_term`.
+ :n:`@one_pattern`.
See :cmd:`Search` for an explanation of the `inside`/`outside` clauses.
@@ -362,11 +362,11 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`).
SearchPattern (?X1 + _ = _ + ?X1).
-.. cmd:: SearchRewrite @one_term {? {| inside | outside } {+ @qualid } }
+.. cmd:: SearchRewrite @one_pattern {? {| inside | outside } {+ @qualid } }
Displays the name and type of all hypotheses of the
selected goal (if any) and theorems of the current context that have the form
- :n:`{? forall {* @binder }, } {* P__i -> } LHS = RHS` where :n:`@one_term`
+ :n:`{? forall {* @binder }, } {* P__i -> } LHS = RHS` where :n:`@one_pattern`
matches either `LHS` or `RHS`.
See :cmd:`Search` for an explanation of the `inside`/`outside` clauses.
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 4ad32e15eb..4c1956d172 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -285,9 +285,12 @@ term_let: [
(* Don't need to document that "( )" is equivalent to "()" *)
| REPLACE "let" [ "(" LIST0 name SEP "," ")" | "()" ] as_return_type ":=" term200 "in" term200
| WITH "let" "(" LIST0 name SEP "," ")" as_return_type ":=" term200 "in" term200
+| MOVETO destructuring_let "let" "(" LIST0 name SEP "," ")" as_return_type ":=" term200 "in" term200
| REPLACE "let" "'" pattern200 ":=" term200 "in" term200
-| WITH "let" "'" pattern200 ":=" term200 OPT case_type "in" term200
+| WITH "let" "'" pattern200 ":=" term200 OPT case_type "in" term200
| DELETE "let" "'" pattern200 ":=" term200 case_type "in" term200
+| MOVETO destructuring_let "let" "'" pattern200 ":=" term200 OPT case_type "in" term200
+| MOVETO destructuring_let "let" "'" pattern200 "in" pattern200 ":=" term200 case_type "in" term200
]
atomic_constr: [
@@ -2478,7 +2481,6 @@ SPLICE: [
| binders
| casted_constr
| check_module_types
-| constr_pattern
| decl_sep
| function_fix_definition (* loses funind annotation *)
| glob
@@ -2652,6 +2654,7 @@ RENAME: [
| ssrfwd ssrdefbody
| ssrclauses ssr_in
| ssrcpat ssrblockpat
+| constr_pattern one_pattern
]
simple_tactic: [
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index c697043f27..26474d950a 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -473,6 +473,10 @@ ssr_dpat: [
term_let: [
| "let" name OPT ( ":" type ) ":=" term "in" term
| "let" name LIST1 binder OPT ( ":" type ) ":=" term "in" term
+| destructuring_let
+]
+
+destructuring_let: [
| "let" "(" LIST0 name SEP "," ")" OPT [ OPT [ "as" name ] "return" term100 ] ":=" term "in" term
| "let" "'" pattern ":=" term OPT ( "return" term100 ) "in" term
| "let" "'" pattern "in" pattern ":=" term "return" term100 "in" term
@@ -724,7 +728,11 @@ sort_family: [
]
hint_info: [
-| "|" OPT natural OPT one_term
+| "|" OPT natural OPT one_pattern
+]
+
+one_pattern: [
+| one_term
]
module_binder: [
@@ -1011,7 +1019,7 @@ command: [
| "Prenex" "Implicits" LIST1 qualid (* SSR plugin *)
| "Print" "Hint" "View" OPT ssrviewpos (* SSR plugin *)
| "Hint" "View" OPT ssrviewpos LIST1 ( one_term OPT ( "|" natural ) ) (* SSR plugin *)
-| "Search" OPT LIST1 ( "-" [ string OPT ( "%" ident ) | one_term ] ) OPT ( "in" LIST1 ( OPT "-" qualid ) ) (* SSR plugin *)
+| "Search" OPT LIST1 ( "-" [ string OPT ( "%" ident ) | one_pattern ] ) OPT ( "in" LIST1 ( OPT "-" qualid ) ) (* SSR plugin *)
| "Typeclasses" "Transparent" LIST1 qualid
| "Typeclasses" "Opaque" LIST1 qualid
| "Typeclasses" "eauto" ":=" OPT "debug" OPT ( "(" [ "bfs" | "dfs" ] ")" ) OPT natural
@@ -1107,9 +1115,9 @@ command: [
| "Compute" term
| "Check" term
| "About" reference OPT univ_name_list
-| "SearchHead" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
-| "SearchPattern" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
-| "SearchRewrite" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "SearchHead" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "SearchPattern" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "SearchRewrite" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
| "Search" LIST1 ( search_query ) OPT ( [ "inside" | "outside" ] LIST1 qualid )
| "Ltac2" OPT "mutable" OPT "rec" tac2def_body LIST0 ( "with" tac2def_body )
| "Ltac2" "Type" OPT "rec" tac2typ_def LIST0 ( "with" tac2typ_def )
@@ -1167,7 +1175,7 @@ search_query: [
search_item: [
| OPT ( [ "head" | "hyp" | "concl" | "headhyp" | "headconcl" ] ":" ) string OPT ( "%" scope_key )
-| OPT ( [ "head" | "hyp" | "concl" | "headhyp" | "headconcl" ] ":" ) one_term
+| OPT ( [ "head" | "hyp" | "concl" | "headhyp" | "headconcl" ] ":" ) one_pattern
| "is" ":" logical_kind
]
@@ -1196,7 +1204,7 @@ hint: [
| "Mode" qualid LIST1 [ "+" | "!" | "-" ]
| "Unfold" LIST1 qualid
| "Constructors" LIST1 qualid
-| "Extern" natural OPT one_term "=>" ltac_expr
+| "Extern" natural OPT one_pattern "=>" ltac_expr
]
tacdef_body: [
@@ -2404,9 +2412,9 @@ tac2mode: [
| "Compute" term
| "Check" term
| "About" reference OPT univ_name_list
-| "SearchHead" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
-| "SearchPattern" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
-| "SearchRewrite" one_term OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "SearchHead" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "SearchPattern" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
+| "SearchRewrite" one_pattern OPT ( [ "inside" | "outside" ] LIST1 qualid )
| "Search" LIST1 ( search_query ) OPT ( [ "inside" | "outside" ] LIST1 qualid )
]
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 01:20:59 +0000