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

(limited to 'pretyping')

diff --git a/pretyping/vernacexpr.ml b/pretyping/vernacexpr.ml
index 4e1c986f1..548689205 100644
--- a/pretyping/vernacexpr.ml
+++ b/pretyping/vernacexpr.ml
@@ -22,6 +22,7 @@ type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation
    make sense to apply a tactic to it. Hence it the types may look very
    similar, they do not seem to mean the same thing. *)
 type goal_selector =
+  | SelectAlreadyFocused
   | SelectNth of int
   | SelectList of (int * int) list
   | SelectId of Id.t
-- 
cgit v1.2.3