From 7c5249278e396740b858b138864eb9d40360b476 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 20 May 2024 11:42:30 +1000 Subject: [PATCH] chore: move release notes about MessageData to v4.9.0 (#4222) --- RELEASES.md | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/RELEASES.md b/RELEASES.md index 118cf027c6..b8c8fccaca 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -22,6 +22,18 @@ v4.9.0 (development in progress) definition itself can be marked as `@[semireducible]` to get the previous behavor. +* The `MessageData.ofPPFormat` constructor has been removed. + Its functionality has been split into two: + + - for lazy structured messages, please use `MessageData.lazy`; + - for embedding `Format` or `FormatWithInfos`, use `MessageData.ofFormatWithInfos`. + + An example migration can be found in [#3929](https://github.com/leanprover/lean4/pull/3929/files#diff-5910592ab7452a0e1b2616c62d22202d2291a9ebb463145f198685aed6299867L109). + +* The `MessageData.ofFormat` constructor has been turned into a function. + If you need to inspect `MessageData`, + you can pattern-match on `MessageData.ofFormatWithInfos`. + v4.8.0 --------- @@ -155,18 +167,6 @@ fact.def : * `Option.toMonad` has been renamed to `Option.getM` and the unneeded `[Monad m]` instance argument has been removed. -* The `MessageData.ofPPFormat` constructor has been removed. - Its functionality has been split into two: - - - for lazy structured messages, please use `MessageData.lazy`; - - for embedding `Format` or `FormatWithInfos`, use `MessageData.ofFormatWithInfos`. - - An example migration can be found in [#3929](https://github.com/leanprover/lean4/pull/3929/files#diff-5910592ab7452a0e1b2616c62d22202d2291a9ebb463145f198685aed6299867L109). - -* The `MessageData.ofFormat` constructor has been turned into a function. - If you need to inspect `MessageData`, - you can pattern-match on `MessageData.ofFormatWithInfos`. - v4.7.0 ---------