From 9126d33ddadf55859500060e9ebc55b006bb9f88 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 13 Apr 2022 09:01:55 -0700
Subject: [PATCH] doc: update release notes

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

diff --git a/RELEASES.md b/RELEASES.md
index 392c28e1c1..567df1ae4f 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -1,6 +1,21 @@
 Unreleased
 ---------
 
+* Remove support for `{}` annotation from inductive datatype contructors. This annotation was barely used, and we can control the binder information for parameter bindings using the new inductive family indices to parameter promotion. Example: the following declaration using `{}`
+```lean
+inductive LE' (n : Nat) : Nat → Prop where
+  | refl {} : LE' n n -- Want `n` to be explicit
+  | succ  : LE' n m → LE' n (m+1)
+```
+can now be written as
+```
+inductive LE' : Nat → Nat → Prop where
+  | refl (n : Nat) : LE' n n
+  | succ : LE' n m → LE' n (m+1)
+```
+In both cases, the inductive family has one parameter and one index.
+Recall that the actual number of parameters can be retrieved using the command `#print`.
+
 * Several improvements to LSP server. Examples: "jump to definition" in mutually recursive sections, fixed incorrect hover information in "match"-expression patterns, "jump to definition" for pattern variables, fixed auto-completion in function headers, etc.
 
 * In `macro ... xs:p* ...` and similar macro bindings of combinators, `xs` now has the correct type `Array Syntax`
@@ -111,6 +126,7 @@ ihr : BST right → Tree.find? (Tree.insert right k v) k = some v
 * (Experimental) New `checkpoint <tactic-seq>` tactic for big interactive proofs.
 
 * Rename tactic `nativeDecide` => `native_decide`.
+
 * Antiquotations are now accepted in any syntax. The `incQuotDepth` `syntax` parser is therefore obsolete and has been removed.
 
 * Renamed tactic `nativeDecide` => `native_decide`.