14 files changed, 83 insertions, 24 deletions
diff --git a/doc/changelog/03-notations/13415-intern-univs.rst b/doc/changelog/03-notations/13415-intern-univs.rst
new file mode 100644
index 0000000000..e9f51461e5
--- /dev/null
+++ b/doc/changelog/03-notations/13415-intern-univs.rst
@@ -0,0 +1,5 @@
+- **Fixed:** Notations understand universe names without getting
+  confused by different imported modules between declaration and use
+  locations (`#13415 <https://github.com/coq/coq/pull/13415>`_, fixes
+  `#13303 <https://github.com/coq/coq/issues/13303>`_, by Gaëtan
+  Gilbert).
diff --git a/doc/changelog/04-tactics/12993-remove-cutrewrite.rst b/doc/changelog/04-tactics/12993-remove-cutrewrite.rst
deleted file mode 100644
index b719c5618e..0000000000
--- a/doc/changelog/04-tactics/12993-remove-cutrewrite.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Removed:**
-  Deprecated ``cutrewrite`` tactic. Use :tacn:`replace` instead
-  (`#12993 <https://github.com/coq/coq/pull/12993>`_,
-  by Théo Zimmermann).
diff --git a/doc/changelog/06-ssreflect/13473-test_pred.rst b/doc/changelog/06-ssreflect/13473-test_pred.rst
new file mode 100644
index 0000000000..3c7df11540
--- /dev/null
+++ b/doc/changelog/06-ssreflect/13473-test_pred.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  Adding a test that the notations `{in _, _}` and `{pred _}` from `ssrbool.v` are displayed correctly.
+  (`#13473 <https://github.com/coq/coq/pull/13473>`_,
+  by Cyril Cohen).
diff --git a/doc/changelog/12-misc/12586-declare+typing_flags.rst b/doc/changelog/12-misc/12586-declare+typing_flags.rst
new file mode 100644
index 0000000000..52915ceee9
--- /dev/null
+++ b/doc/changelog/12-misc/12586-declare+typing_flags.rst
@@ -0,0 +1,6 @@
+- **Added:**
+  Typing flags can now be specified per-constant / inductive, this
+  allows to fine-grain specify them from plugins or attributes. See
+  :ref:`controlling-typing-flags` for details on attribute syntax.
+  (`#12586 <https://github.com/coq/coq/pull/12586>`_,
+  by Emilio Jesus Gallego Arias).
diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst
index 43bbc8b40d..cf46580bdb 100644
--- a/doc/sphinx/language/core/coinductive.rst
+++ b/doc/sphinx/language/core/coinductive.rst
@@ -27,7 +27,8 @@ More information on co-inductive definitions can be found in
 
    This command supports the :attr:`universes(polymorphic)`,
    :attr:`universes(template)`, :attr:`universes(cumulative)`,
-   :attr:`private(matching)`, and :attr:`using` attributes.
+   :attr:`private(matching)`, :attr:`bypass_check(universes)`,
+   :attr:`bypass_check(positivity)`, and :attr:`using` attributes.
 
 .. example::
 
diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst
index 57771c9036..ec5b896dab 100644
--- a/doc/sphinx/language/core/definitions.rst
+++ b/doc/sphinx/language/core/definitions.rst
@@ -90,8 +90,9 @@ Section :ref:`typing-rules`.
    computation on :n:`@term`.
 
    These commands also support the :attr:`universes(polymorphic)`,
-   :attr:`program` (see :ref:`program_definition`),
-   :attr:`canonical` and :attr:`using` attributes.
+   :attr:`program` (see :ref:`program_definition`), :attr:`canonical`,
+   :attr:`bypass_check(universes)`, :attr:`bypass_check(guard)`, and
+   :attr:`using` attributes.
 
    If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode.
    This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic.
@@ -162,7 +163,8 @@ Chapter :ref:`Tactics`. The basic assertion command is:
    correct at some time of the interactive development of a proof, use the
    command :cmd:`Guarded`.
 
-   This command accepts the :attr:`using` attribute.
+   This command accepts the :attr:`bypass_check(universes)`,
+   :attr:`bypass_check(guard)`, and :attr:`using` attributes.
 
    .. exn:: The term @term has type @type which should be Set, Prop or Type.
       :undocumented:
@@ -173,7 +175,8 @@ Chapter :ref:`Tactics`. The basic assertion command is:
       The name you provided is already defined. You have then to choose
       another name.
 
-   .. exn:: Nested proofs are not allowed unless you turn the Nested Proofs Allowed flag on.
+   .. exn:: Nested proofs are discouraged and not allowed by default. This error probably means that you forgot to close the last "Proof." with "Qed." or "Defined.". \
+            If you really intended to use nested proofs, you can do so by turning the "Nested Proofs Allowed" flag on.
 
       You are asserting a new statement while already being in proof editing mode.
       This feature, called nested proofs, is disabled by default.
diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst
index 9fda2ab1fa..4bee7cc1b1 100644
--- a/doc/sphinx/language/core/inductive.rst
+++ b/doc/sphinx/language/core/inductive.rst
@@ -31,7 +31,8 @@ Inductive types
    proposition).
 
    This command supports the :attr:`universes(polymorphic)`,
-   :attr:`universes(template)`, :attr:`universes(cumulative)`, and
+   :attr:`universes(template)`, :attr:`universes(cumulative)`,
+   :attr:`bypass_check(positivity)`, :attr:`bypass_check(universes)`, and
    :attr:`private(matching)` attributes.
 
    Mutually inductive types can be defined by including multiple :n:`@inductive_definition`\s.
@@ -49,10 +50,12 @@ Inductive types
 
    .. exn:: Non strictly positive occurrence of @ident in @type.
 
-      The types of the constructors have to satisfy a *positivity condition*
-      (see Section :ref:`positivity`). This condition ensures the soundness of
-      the inductive definition. The positivity checking can be disabled using
-      the :flag:`Positivity Checking` flag (see :ref:`controlling-typing-flags`).
+      The types of the constructors have to satisfy a *positivity
+      condition* (see Section :ref:`positivity`). This condition
+      ensures the soundness of the inductive definition.
+      Positivity checking can be disabled using the :flag:`Positivity
+      Checking` flag or the :attr:`bypass_check(positivity)` attribute (see
+      :ref:`controlling-typing-flags`).
 
    .. exn:: The conclusion of @type is not valid; it must be built from @ident.
 
@@ -390,7 +393,8 @@ constructions.
    consequently :n:`forall {* @binder }, @type` and its value is equivalent
    to :n:`fun {* @binder } => @term`.
 
-   This command accepts the :attr:`program` attribute.
+   This command accepts the :attr:`program`,
+   :attr:`bypass_check(universes)`, and :attr:`bypass_check(guard)` attributes.
 
    To be accepted, a :cmd:`Fixpoint` definition has to satisfy syntactical
    constraints on a special argument called the decreasing argument. They
@@ -848,9 +852,7 @@ between universes for inductive types in the Type hierarchy.
 
    .. coqtop:: none
 
-      Unset Positivity Checking.
-      Inductive I : Prop := not_I_I (not_I : I -> False) : I.
-      Set Positivity Checking.
+      #[bypass_check(positivity)] Inductive I : Prop := not_I_I (not_I : I -> False) : I.
 
    .. coqtop:: all
 
@@ -884,9 +886,7 @@ between universes for inductive types in the Type hierarchy.
 
    .. coqtop:: none
 
-      Unset Positivity Checking.
-      Inductive Lam := lam (_ : Lam -> Lam).
-      Set Positivity Checking.
+      #[bypass_check(positivity)] Inductive Lam := lam (_ : Lam -> Lam).
 
    .. coqtop:: all
 
@@ -915,9 +915,7 @@ between universes for inductive types in the Type hierarchy.
 
    .. coqtop:: none
 
-      Unset Positivity Checking.
-      Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A.
-      Set Positivity Checking.
+      #[bypass_check(positivity)] Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A.
 
    .. coqtop:: all
 
diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst
index 2460461ede..95c5914e47 100644
--- a/doc/sphinx/language/extensions/arguments-command.rst
+++ b/doc/sphinx/language/extensions/arguments-command.rst
@@ -89,11 +89,25 @@ Setting properties of a function's arguments
          The construct :n:`@name {? % @scope }` declares :n:`@name` as non-implicit if `clear implicits` is specified or at least one other name is declared implicit in the same list of :n:`@name`\s.
          :token:`scope` can be either a scope name or its delimiting key.  See :ref:`binding_to_scope`.
 
+         .. exn:: To rename arguments the 'rename' flag must be specified.
+            :undocumented:
+
+         .. exn:: Flag 'rename' expected to rename @name into @name.
+            :undocumented:
+
       `clear implicits`
          makes all implicit arguments into explicit arguments
+
+         .. exn:: The 'clear implicits' flag must be omitted if implicit annotations are given.
+            :undocumented:
+
       `default implicits`
          automatically determine the implicit arguments of the object.
          See :ref:`auto_decl_implicit_args`.
+
+         .. exn:: The 'default implicits' flag is incompatible with implicit annotations.
+            :undocumented:
+
       `rename`
          rename implicit arguments for the object.  See the example :ref:`here <renaming_implicit_arguments>`.
       `assert`
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index e7db9cfaca..e866e4c624 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1152,6 +1152,12 @@ Controlling Typing Flags
    anymore but it still affects the reduction of the term. Unchecked fixpoints are
    printed by :cmd:`Print Assumptions`.
 
+.. attr:: bypass_check(guard{? = {| yes | no } })
+   :name: bypass_check(guard)
+
+   Similar to :flag:`Guard Checking`, but on a per-declaration
+   basis. Disable guard checking locally with ``bypass_check(guard)``.
+
 .. flag:: Positivity Checking
 
    This flag can be used to enable/disable the positivity checking of inductive
@@ -1159,6 +1165,12 @@ Controlling Typing Flags
    break the consistency of the system, use at your own risk. Unchecked
    (co)inductive types are printed by :cmd:`Print Assumptions`.
 
+.. attr:: bypass_check(positivity{? = {| yes | no } })
+   :name: bypass_check(positivity)
+
+   Similar to :flag:`Positivity Checking`, but on a per-declaration basis.
+   Disable positivity checking locally with ``bypass_check(positivity)``.
+
 .. flag:: Universe Checking
 
    This flag can be used to enable/disable the checking of universes, providing a
@@ -1167,6 +1179,12 @@ Controlling Typing Flags
    :cmd:`Print Assumptions`. It has the same effect as `-type-in-type` command line
    argument (see :ref:`command-line-options`).
 
+.. attr:: bypass_check(universes{? = {| yes | no } })
+   :name: bypass_check(universes)
+
+   Similar to :flag:`Universe Checking`, but on a per-declaration basis.
+   Disable universe checking locally with ``bypass_check(universes)``.
+
 .. cmd:: Print Typing Flags
 
    Print the status of the three typing flags: guard checking, positivity checking
diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst
index 2de6b2a18c..b7f2927000 100644
--- a/doc/sphinx/proofs/writing-proofs/rewriting.rst
+++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst
@@ -146,6 +146,13 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`.
       only in the conclusion of the goal. The clause argument must not contain
       any ``type of`` nor ``value of``.
 
+   .. tacv:: cutrewrite {? {| <- | -> } } (@term__1 = @term__2) {? in @ident }
+      :name: cutrewrite
+
+      .. deprecated:: 8.5
+
+         Use :tacn:`replace` instead.
+
 .. tacn:: subst @ident
    :name: subst
 
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 7201dc6a0e..8ab4265b15 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -709,6 +709,7 @@ through the <tt>Require Import</tt> command.</p>
     theories/Compat/Coq811.v
     theories/Compat/Coq812.v
     theories/Compat/Coq813.v
+    theories/Compat/Coq814.v
   </dd>
 
   <dt> <b>Array</b>:
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 8efda825de..75b3260166 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -1021,6 +1021,9 @@ simple_tactic: [
 | DELETE "unify" constr constr
 | REPLACE "unify" constr constr "with" preident
 | WITH "unify" constr constr OPT ( "with" preident )
+| DELETE "cutrewrite" orient constr
+| REPLACE "cutrewrite" orient constr "in" hyp
+| WITH "cutrewrite" orient constr OPT ( "in" hyp )
 | DELETE "destauto"
 | REPLACE "destauto" "in" hyp
 | WITH "destauto" OPT ( "in" hyp )
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index cf90eea5a1..ccf38d2c15 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1583,6 +1583,8 @@ simple_tactic: [
 | "simple" "injection" destruction_arg
 | "dependent" "rewrite" orient constr
 | "dependent" "rewrite" orient constr "in" hyp
+| "cutrewrite" orient constr
+| "cutrewrite" orient constr "in" hyp
 | "decompose" "sum" constr
 | "decompose" "record" constr
 | "absurd" constr
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 7c709baa48..d950b32160 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -1685,6 +1685,7 @@ simple_tactic: [
 | "einjection" OPT destruction_arg OPT ( "as" LIST0 simple_intropattern )
 | "simple" "injection" OPT destruction_arg
 | "dependent" "rewrite" OPT [ "->" | "<-" ] one_term OPT ( "in" ident )
+| "cutrewrite" OPT [ "->" | "<-" ] one_term OPT ( "in" ident )
 | "decompose" "sum" one_term
 | "decompose" "record" one_term
 | "absurd" one_term