From d94fef210a63db4ff34251afe093041912a7cbde Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 8 Mar 2018 12:45:37 +0100
Subject: Strict focusing using Default Goal Selector.

We add a [SelectAlreadyFocused] constructor to [goal_selector] (read
"!") which causes a failure when there's not exactly 1 goal and
otherwise is a noop.

Then [Set Default Goal Selector "!".] puts us in "strict focusing"
mode where we can only run tactics if we have only one goal or use a
selector.

Closes #6689.
---
 test-suite/success/goal_selector.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/goal_selector.v b/test-suite/success/goal_selector.v
index 8681405175..0951c5c8d4 100644
--- a/test-suite/success/goal_selector.v
+++ b/test-suite/success/goal_selector.v
@@ -53,3 +53,17 @@ Goal True -> exists (x : Prop), x.
 Proof.
   intro H; eexists ?[x]; only [x]: exact True. 1: assumption.
 Qed.
+
+(* Strict focusing! *)
+Set Default Goal Selector "!".
+
+Goal True -> True /\ True /\ True.
+Proof.
+  intro.
+  split;only 2:split.
+  Fail exact I.
+  Fail !:exact I.
+  1:exact I.
+  - !:exact H.
+  - exact I.
+Qed.
-- 
cgit v1.2.3