diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/01-kernel/13563-compact-case-repr.rst | 15 | ||||
| -rw-r--r-- | doc/changelog/04-tactics/13715-lia_implb.rst | 2 | ||||
| -rw-r--r-- | doc/changelog/07-vernac-commands-and-options/13556-master.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/changes.rst | 11 |
4 files changed, 28 insertions, 4 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/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 ------------ |