From a95654a21c350f19ad0da67713359cbf6c49e95a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 1 Jan 2021 16:01:52 +0100 Subject: Document the change of case representation. --- doc/changelog/01-kernel/13563-compact-case-repr.rst | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 doc/changelog/01-kernel/13563-compact-case-repr.rst (limited to 'doc') 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 `_, + fixes `#3166 `_, + by Pierre-Marie Pédrot). -- cgit v1.2.3