Merge PR #13509: Remove compatibility flag Set Bracketing Last Introduction Pattern

Reviewed-by: Zimmi48
Reviewed-by: ppedrot

2 files changed, 6 insertions, 11 deletions

diff --git a/doc/changelog/04-tactics/13509-master+remove-bracketing-last-introduction-pattern-flag.rst b/doc/changelog/04-tactics/13509-master+remove-bracketing-last-introduction-pattern-flag.rst
new file mode 100644
index 0000000000..06c1e280c3
--- /dev/null
+++ b/doc/changelog/04-tactics/13509-master+remove-bracketing-last-introduction-pattern-flag.rst
@@ -0,0 +1,6 @@
+- **Removed:**
+  Deprecated flag ``Bracketing Last Introduction Pattern`` affecting the
+  behavior of trailing disjunctive introduction patterns is
+  definitively removed
+  (`#13509 <https://github.com/coq/coq/pull/13509>`_,
+  by Hugo Herbelin).
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 8f5c045929..d8c4fb61c2 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -264,17 +264,6 @@ These patterns can be used when the hypothesis is an equality:
   :n:`@simple_intropattern_closed`.
   :ref:`Example <intropattern_injection_ex>`
 
-.. flag:: Bracketing Last Introduction Pattern
-
-   For :n:`intros @intropattern_list`, controls how to handle a
-   conjunctive pattern that doesn't give enough simple patterns to match
-   all the arguments in the constructor.  If set (the default), Coq generates
-   additional names to match the number of arguments.
-   Unsetting the flag will put the additional hypotheses in the goal instead, behavior that is more
-   similar to |SSR|'s intro patterns.
-
-   .. deprecated:: 8.10
-
 .. _intropattern_cons_note:
 
 .. note::