From d5c9c90b9760bd51136f0ccbb041f8697ad0a081 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sat, 21 Jul 2018 20:25:27 +0200
Subject: Add support for focusing on named goals using brackets.

---
 vernac/vernacentries.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 9824172315..5258ab2ea4 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1987,8 +1987,9 @@ let vernac_subproof gln =
     match gln with
     | None -> Proof.focus subproof_cond () 1 p
     | Some (Goal_select.SelectNth n) -> Proof.focus subproof_cond () n p
+    | Some (Goal_select.SelectId id) -> Proof.focus_id subproof_cond () id p
     | _ -> user_err ~hdr:"bracket_selector"
-             (str "Brackets only support the single numbered goal selector."))
+             (str "Brackets do not support multi-goal selectors."))
 
 let vernac_end_subproof () =
   Proof_global.simple_with_current_proof (fun _ p ->
-- 
cgit v1.2.3