From 6879320384e63793ff9447d4aaddc919bac540ec Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 30 Mar 2018 16:12:26 +0200
Subject: tclSELECT: SelectAll never happens

---
 tactics/tacticals.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 5e81e2d4b1..8b8d5439b5 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -496,7 +496,7 @@ module New = struct
     | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i
     | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l
     | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id
-    | Vernacexpr.SelectAll -> fun tac -> tac
+    | Vernacexpr.SelectAll -> anomaly ~label:"tclSELECT" Pp.(str "SelectAll not allowed here")
 
   (* Check that holes in arguments have been resolved *)
 
-- 
cgit v1.2.3


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.
---
 tactics/tacticals.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'tactics')

diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 8b8d5439b5..82b178388e 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