12 files changed, 52 insertions, 10 deletions
diff --git a/doc/changelog/01-kernel/13563-compact-case-repr.rst b/doc/changelog/01-kernel/13563-compact-case-repr.rst
new file mode 100644
index 0000000000..c8ee9bc1e6
--- /dev/null
+++ b/doc/changelog/01-kernel/13563-compact-case-repr.rst
@@ -0,0 +1,15 @@
+- **Changed:**
+  The term representation of pattern-matchings now uses a compact form that
+  provides a few static guarantees such as eta-expansion of branches and return
+  clauses and is usually more efficient. The most visible user change is that for
+  the time being, the :tacn:`destruct` tactic and its variants generate dummy
+  cuts (β redexes) in the branches of the generated proof.
+  This can also generate very uncommon backwards incompatibilities, such as a
+  change of occurrence numbering for subterms, or breakage of unification in
+  complex situations involving pattern-matchings whose underlying inductive type
+  declares let-bindings in parameters, arity or constructor types. For ML plugin
+  developers, an in-depth description of the new representation, as well as
+  porting tips, can be found in dev/doc/case-repr.md
+  (`#13563 <https://github.com/coq/coq/pull/13563>`_,
+  fixes `#3166 <https://github.com/coq/coq/issues/3166>`_,
+  by Pierre-Marie Pédrot).
diff --git a/doc/changelog/04-tactics/13469-no-int-in-fail.rst b/doc/changelog/04-tactics/13469-no-int-in-fail.rst
new file mode 100644
index 0000000000..e0fcbb924e
--- /dev/null
+++ b/doc/changelog/04-tactics/13469-no-int-in-fail.rst
@@ -0,0 +1,5 @@
+- **Removed:**
+  :tacn:`fail` and :tacn:`gfail`, which formerly accepted negative
+  values as a parameter, now give syntax errors for negative
+  values (`#13469 <https://github.com/coq/coq/pull/13469>`_,
+  by Jim Fehrle).
diff --git a/doc/changelog/04-tactics/13696-deprecate_at_in_conversion.rst b/doc/changelog/04-tactics/13696-deprecate_at_in_conversion.rst
new file mode 100644
index 0000000000..306fe8052d
--- /dev/null
+++ b/doc/changelog/04-tactics/13696-deprecate_at_in_conversion.rst
@@ -0,0 +1,7 @@
+- **Deprecated:**
+  In :tacn:`change` and :tacn:`change_no_check`, the
+  `at ... with ...` form is deprecated.  Use
+  `with ... at ...` instead.  For `at ... with ... in H |-`,
+  use `with ... in H at ... |-`.
+  (`#13696 <https://github.com/coq/coq/pull/13696>`_,
+  by Jim Fehrle).
diff --git a/doc/changelog/04-tactics/13715-lia_implb.rst b/doc/changelog/04-tactics/13715-lia_implb.rst
new file mode 100644
index 0000000000..dd61872342
--- /dev/null
+++ b/doc/changelog/04-tactics/13715-lia_implb.rst
@@ -0,0 +1,2 @@
+- **Added:**
+  :tacn:`lia` supports the boolean operator `Bool.implb` (`#13715 <https://github.com/coq/coq/pull/13715>`_, by Frédéric Besson).
diff --git a/doc/changelog/07-vernac-commands-and-options/13556-master.rst b/doc/changelog/07-vernac-commands-and-options/13556-master.rst
deleted file mode 100644
index 05a60026a3..0000000000
--- a/doc/changelog/07-vernac-commands-and-options/13556-master.rst
+++ /dev/null
@@ -1,4 +0,0 @@
-- **Changed:**
-  The warning `custom-entry-overriden` has been renamed to `custom-entry-overridden` (with two d's).
-  (`#13556 <https://github.com/coq/coq/pull/13556>`_,
-  by Simon Friis Vindum).
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index b9a3c1973c..d9e4e4f2b3 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -690,6 +690,17 @@ Infrastructure and dependencies
   by Emilio Jesus Gallego Arias and Vicent Laporte, with help from
   Frédéric Besson).
 
+Changes in 8.13.0
+~~~~~~~~~~~~~~~~~
+
+Commands and options
+^^^^^^^^^^^^^^^^^^^^
+
+- **Changed:**
+  The warning `custom-entry-overriden` has been renamed to `custom-entry-overridden` (with two d's).
+  (`#13556 <https://github.com/coq/coq/pull/13556>`_,
+  by Simon Friis Vindum).
+
 Version 8.12
 ------------
 
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index e2e37ec438..edbc89aad8 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -490,3 +490,6 @@ epub_exclude_files = ['search.html']
 
 # navtree options
 navtree_shift = True
+
+# since sphinxcontrib-bibtex version 2 we need this
+bibtex_bibfiles = [ "biblio.bib" ]
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 8b627c29a4..013ff0a83f 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -879,7 +879,7 @@ Print/identity tactic: idtac
 Failing
 ~~~~~~~
 
-.. tacn:: {| fail | gfail } {? @int_or_var } {* {| @ident | @string | @natural } }
+.. tacn:: {| fail | gfail } {? @nat_or_var } {* {| @ident | @string | @natural } }
    :name: fail; gfail
 
    :tacn:`fail` is the always-failing tactic: it does not solve any
@@ -900,7 +900,7 @@ Failing
    tactic into the goals, meaning that if there are no goals when it is
    evaluated, a tactic call like :tacn:`let` :n:`x := H in` :tacn:`fail` `0 x` will succeed.
 
-   :n:`@int_or_var`
+   :n:`@nat_or_var`
       The failure level. If no level is specified, it defaults to 0.
       The level is used by :tacn:`try`, :tacn:`repeat`, :tacn:`match goal` and the branching
       tacticals. If 0, it makes :tacn:`match goal` consider the next clause
diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst
index 07b7928847..8873d02888 100644
--- a/doc/sphinx/proofs/writing-proofs/rewriting.rst
+++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst
@@ -280,6 +280,9 @@ Rewriting with definitional equality
      whose value which will substituted for `x` in :n:`@one_term__to`, such as in
      `change (f ?x ?y) with (g (x, y))` or `change (fun x => ?f x) with f`.
 
+     The `at ... with ...` form is deprecated in 8.14; use `with ... at ...` instead.
+     For `at ... with ... in H |-`, use `with ... in H at ... |-`.
+
    :n:`@occurrences`
      If `with` is not specified, :n:`@occurrences` must only specify
      entire hypotheses and/or the goal; it must not include any
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index f267cdb697..44bb767011 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -864,8 +864,8 @@ ltac_expr1: [
 | EDIT match_key ADD_OPT "reverse" "goal" "with" match_context_list "end"
 | MOVETO simple_tactic match_key OPT "reverse" "goal" "with" match_context_list "end"
 | MOVETO simple_tactic match_key ltac_expr5 "with" match_list "end"
-| REPLACE failkw [ int_or_var | ] LIST0 message_token
-| WITH failkw OPT int_or_var LIST0 message_token
+| REPLACE failkw [ nat_or_var | ] LIST0 message_token
+| WITH failkw OPT nat_or_var LIST0 message_token
 | REPLACE reference LIST0 tactic_arg
 | WITH reference LIST1 tactic_arg
 | l1_tactic
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index ccf38d2c15..9f2559ffbc 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -2095,7 +2095,7 @@ ltac_expr1: [
 | "first" "[" LIST0 ltac_expr5 SEP "|" "]"
 | "solve" "[" LIST0 ltac_expr5 SEP "|" "]"
 | "idtac" LIST0 message_token
-| failkw [ int_or_var | ] LIST0 message_token
+| failkw [ nat_or_var | ] LIST0 message_token
 | simple_tactic
 | tactic_value
 | reference LIST0 tactic_arg
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 72e101446c..b53af609ec 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -1653,7 +1653,7 @@ simple_tactic: [
 | "first" "[" LIST0 ltac_expr SEP "|" "]"
 | "solve" "[" LIST0 ltac_expr SEP "|" "]"
 | "idtac" LIST0 [ ident | string | natural ]
-| [ "fail" | "gfail" ] OPT int_or_var LIST0 [ ident | string | natural ]
+| [ "fail" | "gfail" ] OPT nat_or_var LIST0 [ ident | string | natural ]
 | ltac_expr ssrintros      (* SSR plugin *)
 | "fun" LIST1 name "=>" ltac_expr
 | "eval" red_expr "in" term