From a71ac77f94936319e7e47bedecb44c2b75f73d5e Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Fri, 17 Aug 2018 17:53:55 +0200
Subject: Document focusing on named goals.

---
 CHANGES | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'CHANGES')

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,
-- 
cgit v1.2.3