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.

1 files changed, 2 insertions, 2 deletions

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index e88284fb1c..27c46fe4e3 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -91,7 +91,7 @@ open Decl_kinds
 
   let sep_end = function
     | VernacBullet _
-    | VernacSubproof None
+    | VernacSubproof _
     | VernacEndSubproof -> str""
     | _ -> str"."
 
@@ -1199,7 +1199,7 @@ open Decl_kinds
       | VernacSubproof None ->
         return (str "{")
       | VernacSubproof (Some i) ->
-        return (keyword "BeginSubproof" ++ spc () ++ int i)
+        return (Proof_bullet.pr_goal_selector i ++ str ":" ++ spc () ++ str "{")
       | VernacEndSubproof ->
         return (str "}")