change the CHANGELOG

CHANGELOG.md

@@ -35,8 +35,8 @@ lemma.
   Mansky)
 * Remove the `bool`-valued `stuckness_leb`; use `stuckness_le` (in `Prop`)
   instead.
-* Improve `iNext` to support the removal of later modality by the later credit
-  when the goal can add the fancy update.
+* Add support for `iNext credit:"H"` which will use a later credit to strip a later.
+  (by @ffengyu)
 
 **Changes in `proofmode`:**
 
@@ -47,8 +47,8 @@ lemma.
 **Changes in `heap_lang`:**
 
 * Add `Inhabited lock_name` to `lock` class. (by Daniel Nezamabadi)
-* Improve `wp_pure credit: H` to bump up the later credit by 1 when `H` is an
-  existing credit.
+* Improve `wp_pure credit:"H"` so that if "H" is an existing credit, it gets
+  incremented by 1. (by @ffengyu)
 
 **Infrastructure:**