13 files changed, 106 insertions, 46 deletions
diff --git a/doc/changelog/02-specification-language/13911-master.rst b/doc/changelog/02-specification-language/13911-master.rst
new file mode 100644
index 0000000000..a0b37dd2d9
--- /dev/null
+++ b/doc/changelog/02-specification-language/13911-master.rst
@@ -0,0 +1,4 @@
+- **Removed:**
+  The little used `:>` type cast, which was only interpreted in Program-mode
+  (`#13911 <https://github.com/coq/coq/pull/13911>`_,
+  by Jim Fehrle and Théo Zimmermann).
diff --git a/doc/changelog/03-notations/13965-syndef-principal-scope.rst b/doc/changelog/03-notations/13965-syndef-principal-scope.rst
new file mode 100644
index 0000000000..448dbbe3c7
--- /dev/null
+++ b/doc/changelog/03-notations/13965-syndef-principal-scope.rst
@@ -0,0 +1,12 @@
+- **Added:**
+  Let the user specify a scope for abbreviation arguments, e.g.
+  ``Notation abbr X := t (X in scope my_scope)``.
+  (`#13965 <https://github.com/coq/coq/pull/13965>`_,
+  by Enrico Tassi).
+- **Changed:**
+  The error ``Argument X was previously inferred to be in scope
+  XXX_scope but is here used in YYY_scope.`` is now the warning
+  ``[inconsistent-scopes,syntax]`` and can be silenced by
+  specifying the scope of the argument
+  (`#13965 <https://github.com/coq/coq/pull/13965>`_,
+  by Enrico Tassi).
diff --git a/doc/changelog/05-tactic-language/14094-ltac2-notation-level-fix.rst b/doc/changelog/05-tactic-language/14094-ltac2-notation-level-fix.rst
new file mode 100644
index 0000000000..41bc3329c1
--- /dev/null
+++ b/doc/changelog/05-tactic-language/14094-ltac2-notation-level-fix.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+  Ltac2 notations now correctly take into account their assigned level
+  (`#14094 <https://github.com/coq/coq/pull/14094>`_,
+  fixes `#11866 <https://github.com/coq/coq/issues/11866>`_,
+  by Pierre-Marie Pédrot).
diff --git a/doc/changelog/05-tactic-language/14128-ltac2-bool-equal-rename.rst b/doc/changelog/05-tactic-language/14128-ltac2-bool-equal-rename.rst
new file mode 100644
index 0000000000..17eb710344
--- /dev/null
+++ b/doc/changelog/05-tactic-language/14128-ltac2-bool-equal-rename.rst
@@ -0,0 +1,5 @@
+- **Changed:**
+  Renamed Ltac2 Bool.eq into Bool.equal for uniformity.
+  The old function is now a deprecated alias
+  (`#14128 <https://github.com/coq/coq/pull/14128>`_,
+  by Pierre-Marie Pédrot).
diff --git a/doc/changelog/12-misc/14041-cs_lambda.rst b/doc/changelog/12-misc/14041-cs_lambda.rst
new file mode 100644
index 0000000000..872b1f09eb
--- /dev/null
+++ b/doc/changelog/12-misc/14041-cs_lambda.rst
@@ -0,0 +1,6 @@
+- **Added:**
+  Enable canonical `fun _ => _` projections,
+  see :ref:`canonicalstructures` for details.
+  (`#14041 <https://github.com/coq/coq/pull/14041>`_,
+  by Jan-Oliver Kaiser and Pierre Roux,
+  reviewed by Cyril Cohen and Enrico Tassi).
diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst
index a011c81f15..52e47b52ae 100644
--- a/doc/sphinx/addendum/program.rst
+++ b/doc/sphinx/addendum/program.rst
@@ -135,17 +135,6 @@ use the :g:`dec` combinator to get the correct hypotheses as in:
 The :g:`let` tupling construct :g:`let (x1, ..., xn) := t in b` does not
 produce an equality, contrary to the let pattern construct
 :g:`let '(x1,..., xn) := t in b`.
-Also, :g:`term :>` explicitly asks the system to
-coerce term to its support type. It can be useful in notations, for
-example:
-
-.. coqtop:: all
-
-   Notation " x `= y " := (@eq _ (x :>) (y :>)) (only parsing).
-
-This notation denotes equality on subset types using equality on their
-support types, avoiding uses of proof-irrelevance that would come up
-when reasoning with equality on the subset types themselves.
 
 The next two commands are similar to their standard counterparts
 :cmd:`Definition` and :cmd:`Fixpoint`
diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst
index fcf61a5bf4..1a729ced4e 100644
--- a/doc/sphinx/language/core/definitions.rst
+++ b/doc/sphinx/language/core/definitions.rst
@@ -42,7 +42,6 @@ Type cast
    term_cast ::= @term10 : @type
    | @term10 <: @type
    | @term10 <<: @type
-   | @term10 :>
 
 The expression :n:`@term10 : @type` is a type cast expression. It enforces
 the type of :n:`@term10` to be :n:`@type`.
@@ -53,9 +52,6 @@ to type check that :n:`@term10` has type :n:`@type` (see :tacn:`vm_compute`).
 :n:`@term10 <<: @type` specifies that compilation to OCaml will be used
 to type check that :n:`@term10` has type :n:`@type` (see :tacn:`native_compute`).
 
-:n:`@term10 :>` casts to the support type in Program mode.
-See :ref:`syntactic_control`.
-
 .. _gallina-definitions:
 
 Top-level definitions
diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst
index fbba6c30b8..e3b014d8d5 100644
--- a/doc/sphinx/language/extensions/canonical.rst
+++ b/doc/sphinx/language/extensions/canonical.rst
@@ -41,12 +41,54 @@ in :ref:`canonicalstructures`; here only a simple example is given.
    This command supports the :attr:`local` attribute.  When used, the
    structure is canonical only within the :cmd:`Section` containing it.
 
-   Assume that :token:`qualid` denotes an object ``(Build_struct`` |c_1| … |c_n| ``)`` in the
-   structure :g:`struct` of which the fields are |x_1|, …, |x_n|.
-   Then, each time an equation of the form ``(``\ |x_i| ``_)`` |eq_beta_delta_iota_zeta| |c_i| has to be
+   :token:`qualid` (in :token:`reference`) denotes an object :n:`(Build_struct c__1 … c__n)` in the
+   structure :g:`struct` for which the fields are :n:`x__1, …, x__n`.
+   Then, each time an equation of the form :n:`(x__i _)` |eq_beta_delta_iota_zeta| :n:`c__i` has to be
    solved during the type checking process, :token:`qualid` is used as a solution.
-   Otherwise said, :token:`qualid` is canonically used to extend the field |c_i|
-   into a complete structure built on |c_i|.
+   Otherwise said, :token:`qualid` is canonically used to extend the field :n:`x__i`
+   into a complete structure built on :n:`c__i` when :n:`c__i` unifies with :n:`(x__i _)`.
+
+   The following kinds of terms are supported for the fields :n:`c__i` of :token:`qualid`:
+
+   * :term:`Constants <constant>` and section variables of an active section,
+     applied to zero or more arguments.
+   * :token:`sort`\s.
+   * Literal functions:  `fun … => …`.
+   * Literal, non-dependent function types, i.e. implications: `… -> …`.
+   * Variables bound in :token:`qualid`.
+
+   Only the head symbol of an existing instance's field :n:`c__i`
+   is considered when searching for a canonical extension.
+   We call this head symbol the *key* and we say ":token:`qualid` *keys* the field :n:`x__i` to :n:`k`" when :n:`c__i`'s
+   head symbol is :n:`k`.
+   Keys are the only piece of information that is used for canonical extension.
+   The keys corresponding to the kinds of terms listed above are:
+
+   * For constants and section variables, potentially applied to arguments:
+     the constant or variable itself, disregarding any arguments.
+   * For sorts: the sort itself.
+   * For literal functions: skip the abstractions and use the key of the body.
+   * For literal functions types: a disembodied implication key denoted `_ -> _`, disregarding both its
+     domain and codomain.
+   * For variables bound in :token:`qualid`: a catch-all key denoted `_`.
+
+   This means that, for example, `(some_constant x1)` and `(some_constant (other_constant y1 y2) x2)`
+   are not distinct keys.
+
+   Variables bound in :token:`qualid` match any term for the purpose of canonical extension.
+   This has two major consequences for a field :n:`c__i` keyed to a variable of :token:`qualid`:
+
+   1. Unless another key—and, thus, instance—matches :n:`c__i`, the instance will always be considered by
+      unification.
+   2. :n:`c__i` will be considered overlapping not distinct from any other canonical instance
+      that keys :n:`x__i` to one of its own variables.
+
+   A record field :n:`x__i` can only be keyed once to each key.
+   Coq prints a warning when :token:`qualid` keys :n:`x__i` to a term
+   whose head symbol is already keyed by an existing canonical instance.
+   In this case, Coq will not register that :token:`qualid` as a canonical
+   extension.
+   (The remaining fields of the instance can still be used for canonical extension.)
 
    Canonical structures are particularly useful when mixed with coercions
    and strict implicit arguments.
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst
index 25ac72069b..52cf565998 100644
--- a/doc/sphinx/proof-engine/ltac2.rst
+++ b/doc/sphinx/proof-engine/ltac2.rst
@@ -1251,6 +1251,10 @@ Notations
 
    This command supports the :attr:`deprecated` attribute.
 
+   .. exn:: Notation levels must range between 0 and 6.
+
+      The level of a notation must be an integer between 0 and 6 inclusive.
+
 Abbreviations
 ~~~~~~~~~~~~~
 
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index d212256765..f65361bc64 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -1182,7 +1182,7 @@ Here are the syntax elements used by the various notation commands.
    .. prodn::
       syntax_modifier ::= at level @natural
       | in custom @ident {? at level @natural }
-      | {+, @ident } at @level
+      | {+, @ident } {| at @level | in scope @ident }
       | @ident at @level {? @binder_interp }
       | @ident @explicit_subentry
       | @ident @binder_interp
@@ -1374,6 +1374,10 @@ interpreted in the scope stack extended with the scope bound to :n:`@scope_key`.
 
    Removes the delimiting keys associated with a scope.
 
+The arguments of an :ref:`abbreviation <Abbreviations>` can be interpreted
+in a scope stack locally extended with a given scope by using the modifier
+:n:`{+, @ident } in scope @scope_name`.s
+
 Binding types or coercion classes to a notation scope
 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
 
@@ -1567,7 +1571,7 @@ Displaying information about scopes
 Abbreviations
 --------------
 
-.. cmd:: Notation @ident {* @ident__parm } := @one_term {? ( only parsing ) }
+.. cmd:: Notation @ident {* @ident__parm } := @one_term {? ( {+, @syntax_modifier } ) }
    :name: Notation (abbreviation)
 
    .. todo: for some reason, Sphinx doesn't complain about a duplicate name if
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index fd1c3c0260..48d399dfd3 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -365,7 +365,6 @@ term100: [
 | REPLACE term99 ":" term200
 | WITH term99 ":" type
 | MOVETO term_cast term99 ":" type
-| MOVETO term_cast term99 ":>"
 ]
 
 constr: [
@@ -1410,8 +1409,9 @@ syntax_modifier: [
 | DELETE "in" "custom" IDENT
 | REPLACE "in" "custom" IDENT; "at" "level" natural
 | WITH "in" "custom" IDENT OPT ( "at" "level" natural )
-| REPLACE IDENT; "," LIST1 IDENT SEP "," "at" level
-| WITH LIST1 IDENT SEP "," "at" level
+| DELETE IDENT; "in" "scope" IDENT
+| REPLACE IDENT; "," LIST1 IDENT SEP "," [ "at" level | "in" "scope" IDENT ]
+| WITH LIST1 IDENT SEP "," [ "at" level | "in" "scope" IDENT ]
 ]
 
 explicit_subentry: [
@@ -2643,7 +2643,6 @@ SPLICE: [
 | quoted_attributes  (* todo: splice or not? *)
 | printable
 | hint
-| only_parsing
 | record_fields
 | constructor_type
 | record_binder
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 0c8980b1bd..b5a234a86a 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1,6 +1,15 @@
 (* Coq grammar generated from .mlg files.  Do not edit by hand.  Not compiled into Coq *)
 DOC_GRAMMAR
 
+vernac_toplevel: [
+| "Drop" "."
+| "Quit" "."
+| "BackTo" natural "."
+| test_show_goal "Show" "Goal" natural "at" natural "."
+| "Show" "Proof" "Diffs" OPT "removed" "."
+| Pvernac.Vernac_.main_entry
+]
+
 Constr.ident: [
 | Prim.ident
 ]
@@ -75,7 +84,6 @@ term100: [
 | term99 "<:" term200
 | term99 "<<:" term200
 | term99 ":" term200
-| term99 ":>"
 | term99
 ]
 
@@ -478,15 +486,6 @@ strategy_level: [
 | "transparent"
 ]
 
-vernac_toplevel: [
-| "Drop" "."
-| "Quit" "."
-| "BackTo" natural "."
-| test_show_goal "Show" "Goal" natural "at" natural "."
-| "Show" "Proof" "Diffs" OPT "removed" "."
-| Pvernac.Vernac_.main_entry
-]
-
 opt_hintbases: [
 |
 | ":" LIST1 IDENT
@@ -1401,18 +1400,13 @@ syntax: [
 | "Undelimit" "Scope" IDENT
 | "Bind" "Scope" IDENT; "with" LIST1 class_rawexpr
 | "Infix" ne_lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ]
-| "Notation" identref LIST0 ident ":=" constr only_parsing
+| "Notation" identref LIST0 ident ":=" constr syntax_modifiers
 | "Notation" lstring ":=" constr syntax_modifiers OPT [ ":" IDENT ]
 | "Format" "Notation" STRING STRING STRING
 | "Reserved" "Infix" ne_lstring syntax_modifiers
 | "Reserved" "Notation" ne_lstring syntax_modifiers
 ]
 
-only_parsing: [
-| "(" "only" "parsing" ")"
-|
-]
-
 level: [
 | "level" natural
 | "next" "level"
@@ -1428,8 +1422,9 @@ syntax_modifier: [
 | "only" "printing"
 | "only" "parsing"
 | "format" STRING OPT STRING
-| IDENT; "," LIST1 IDENT SEP "," "at" level
+| IDENT; "," LIST1 IDENT SEP "," [ "at" level | "in" "scope" IDENT ]
 | IDENT; "at" level OPT binder_interp
+| IDENT; "in" "scope" IDENT
 | IDENT binder_interp
 | IDENT explicit_subentry
 ]
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 40bb980e90..cd96693bf0 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -553,7 +553,6 @@ term_cast: [
 | term10 ":" type
 | term10 "<:" type
 | term10 "<<:" type
-| term10 ":>"
 ]
 
 term_match: [
@@ -1096,7 +1095,7 @@ command: [
 | "Undelimit" "Scope" scope_name
 | "Bind" "Scope" scope_name "with" LIST1 class
 | "Infix" string ":=" one_term OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) OPT [ ":" scope_name ]
-| "Notation" ident LIST0 ident ":=" one_term OPT ( "(" "only" "parsing" ")" )
+| "Notation" ident LIST0 ident ":=" one_term OPT ( "(" LIST1 syntax_modifier SEP "," ")" )
 | "Notation" string ":=" one_term OPT ( "(" LIST1 syntax_modifier SEP "," ")" ) OPT [ ":" scope_name ]
 | "Format" "Notation" string string string
 | "Reserved" "Infix" string OPT ( "(" LIST1 syntax_modifier SEP "," ")" )
@@ -1540,7 +1539,7 @@ class: [
 syntax_modifier: [
 | "at" "level" natural
 | "in" "custom" ident OPT ( "at" "level" natural )
-| LIST1 ident SEP "," "at" level
+| LIST1 ident SEP "," [ "at" level | "in" "scope" ident ]
 | ident "at" level OPT binder_interp
 | ident explicit_subentry
 | ident binder_interp