From d94fef210a63db4ff34251afe093041912a7cbde Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
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.
---
 tactics/tacticals.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'tactics')

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 8b8d5439b..82b178388 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -497,6 +497,8 @@ module New = struct
     | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l
     | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id
     | Vernacexpr.SelectAll -> anomaly ~label:"tclSELECT" Pp.(str "SelectAll not allowed here")
+    | Vernacexpr.SelectAlreadyFocused ->
+      anomaly ~label:"tclSELECT" Pp.(str "SelectAlreadyFocused not allowed here")
 
   (* Check that holes in arguments have been resolved *)
 
-- 
cgit v1.2.3