From f33cb27d1c7cb61ba2c00cdb2299f42bf3d4f40b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 14 Feb 2022 15:58:58 -0800
Subject: [PATCH] doc: update `RELEASES.md`

---
 RELEASES.md | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/RELEASES.md b/RELEASES.md
index 1052f81e19..728a7746df 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -36,3 +36,23 @@ def concat : List ((α : Type) × ToString α × α) → String
   | [] => ""
   | ⟨_, _, a⟩ :: as => toString a ++ concat as
 ```
+
+* Notation for providing the motive for `match` expressions has changed.
+Before:
+```lean
+match x, rfl : (y : Nat) → x = y → Nat with
+| 0,   h => ...
+| x+1, h => ...
+```
+Now:
+```lean
+match (motive := (y : Nat) → x = y → Nat) x, rfl with
+| 0,   h => ...
+| x+1, h => ...
+```
+With this change, the notation for giving names to equality proofs in `match`-expressions is not whitespace sensitive anymore. That is,
+we can now write
+```lean
+match h : sort.swap a b with
+| (r₁, r₂) => ... -- `h : sort.swap a b = (r₁, r₂)`
+```