Merge PR #13563: Revival of #9710 (Compact kernel representation of pattern-matching)

Reviewed-by: mattam82
Reviewed-by: SkySkimmer
Ack-by: gares
Ack-by: jfehrle

1 files changed, 15 insertions, 0 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).