Document focusing on named goals.

1 files changed, 6 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index df4a1df176..a704f8047b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -48,6 +48,12 @@ Tactics
   may need to add `Require Import Lra` to your developments. For compatibility,
   we now define `fourier` as a deprecated alias of `lra`.
 
+Focusing
+
+- Focusing bracket `{` now supports named goal selectors,
+  e.g. `[x]: {` will focus on a goal (existential variable) named `x`.
+  As usual, unfocus with `}` once the sub-goal is fully solved.
+
 Standard Library
 
 - Added `Ascii.eqb` and `String.eqb` and the `=?` notation for them,