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.
---
 intf/vernacexpr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index 5106e513b9..bc7b0585d4 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -451,7 +451,7 @@ type vernac_expr =
   | VernacUnfocus
   | VernacUnfocused
   | VernacBullet of bullet
-  | VernacSubproof of int option
+  | VernacSubproof of goal_selector option
   | VernacEndSubproof
   | VernacShow of showable
   | VernacCheckGuard
-- 
cgit v1.2.3