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.
---
 printing/ppvernac.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'printing')

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 "}")
 
-- 
cgit v1.2.3