From 7a7e39f8a0279a149c6b7c20f026cb629aa489f7 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Fri, 17 Aug 2018 18:11:47 +0200
Subject: Update test-suite for focusing on named goals.

---
 test-suite/success/BracketsWithGoalSelector.v | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/BracketsWithGoalSelector.v b/test-suite/success/BracketsWithGoalSelector.v
index ed035f5213..2f7425bce6 100644
--- a/test-suite/success/BracketsWithGoalSelector.v
+++ b/test-suite/success/BracketsWithGoalSelector.v
@@ -14,3 +14,12 @@ Proof.
 Fail Qed.
   }
 Qed.
+
+Lemma foo (n: nat) (P : nat -> Prop):
+  P n.
+Proof.
+  intros.
+  refine (nat_ind _ ?[Base] ?[Step] _).
+  [Base]: { admit. }
+  [Step]: { admit. }
+Abort.
-- 
cgit v1.2.3