From 3a447d83226c4591e796e44933dad8278d97d683 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Fri, 5 Jan 2018 12:57:56 +0100
Subject: Brackets support single numbered goal selectors.

This allows to focus on a sub-goal other than the first one without
resorting to the `Focus` command.
---
 vernac/vernacentries.ml | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ded0d97e64..bccde169f2 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1846,11 +1846,8 @@ let vernac_unfocused () =
     user_err Pp.(str "The proof is not fully unfocused.")
 
 
-(* BeginSubproof / EndSubproof. 
-    BeginSubproof (vernac_subproof) focuses on the first goal, or the goal
-    given as argument.
-    EndSubproof (vernac_end_subproof) unfocuses from a BeginSubproof, provided
-    that the proof of the goal has been completed.
+(* "{" focuses on the first goal, "n: {" focuses on the n-th goal
+    "}" unfocuses, provided that the proof of the goal has been completed.
 *)
 let subproof_kind = Proof.new_focus_kind ()
 let subproof_cond = Proof.done_cond subproof_kind
@@ -1859,7 +1856,9 @@ let vernac_subproof gln =
   Proof_global.simple_with_current_proof (fun _ p ->
     match gln with
     | None -> Proof.focus subproof_cond () 1 p
-    | Some n -> Proof.focus subproof_cond () n p)
+    | Some (SelectNth n) -> Proof.focus subproof_cond () n p
+    | _ -> user_err ~hdr:"bracket_selector"
+             (str "Brackets only support the single numbered goal selector."))
 
 let vernac_end_subproof () =
   Proof_global.simple_with_current_proof (fun _ p ->
-- 
cgit v1.2.3