From aa2d547c2bbbb4f41d8f042ded1a4340247cd53e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 7 Feb 2022 17:26:43 -0800
Subject: [PATCH] doc: add last item at congr theorem whishlist

closes #988
---
 RELEASES.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/RELEASES.md b/RELEASES.md
index 7991eeaf56..efa65737ef 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -19,3 +19,5 @@ theorem dep_congr [DecidableEq ι] {p : ι → Set α} [∀ i, Inhabited (p i)]
 * [Remove deprecated leanpkg](https://github.com/leanprover/lean4/pull/985) in favor of [Lake](https://github.com/leanprover/lake) now bundled with Lean.
 
 * Various improvements to go-to-definition & find-all-references accuracy.
+
+* Auto generated congruence lemmas with support for casts on proofs and `Decidable` instances (see [whishlist](https://github.com/leanprover/lean4/issues/988)).