From d473cc5a4cce6353a5e5d19b6d49772da69b5eb7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 1 Apr 2022 11:38:50 -0700
Subject: [PATCH] chore: update release notes for issue #1090

closes #1090
---
 RELEASES.md | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/RELEASES.md b/RELEASES.md
index b1968cd8ba03..e513185f8168 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -1,9 +1,20 @@
 Unreleased
 ---------
 
+* [Fix inconsistency between `syntax` and kind names](https://github.com/leanprover/lean4/issues/1090).
+  The node kinds `numLit`, `charLit`, `nameLit`, `strLit`, and `scientificLit` are now called
+  `num`, `char`, `name`, `str`, and `scientific` respectively. Example: we now write
+  ```lean
+  macro_rules | `($n:num) => `("hello")
+  ```
+  instead of
+  ```lean
+  macro_rules | `($n:numLit) => `("hello")
+  ```
+
 * (Experimental) New `checkpoint <tactic-seq>` tactic for big interactive proofs.
 
-* Renamed tactic `nativeDecide` => `native_decide`.
+* Rename tactic `nativeDecide` => `native_decide`.
 
 * "Cleanup" local context before elaborating a `match` alternative right-hand-side. Examples:
 ```lean