Merge PR #6944: Strict focusing using Default Goal Selector.

12 files changed, 63 insertions, 9 deletions

diff --git a/CHANGES b/CHANGES
index 2db8ace96a..a270aef96d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,6 +1,12 @@
 Changes from 8.8.2 to 8.9+beta1
 ===============================
 
+Tactics
+
+- Added toplevel goal selector ! which expects a single focused goal.
+  Use with Set Default Goal Selector to force focusing before tactics
+  are called.
+
 Tools
 
 - Coq_makefile lets one override or extend the following variables from
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 009758319b..7ab11889f5 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -272,6 +272,12 @@ focused goals with:
       In this variant, :n:`@expr` is applied to all focused goals. ``all:`` can only
       be used at the toplevel of a tactic expression.
 
+   .. tacv:: !: @expr
+
+      In this variant, if exactly one goal is focused :n:`expr` is
+      applied to it. Otherwise the tactical fails. ``!:`` can only be
+      used at the toplevel of a tactic expression.
+
    .. tacv:: par: @expr
 
       In this variant, :n:`@expr` is applied to all focused goals in parallel.
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 7a45272f25..a3d06ae046 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -53,13 +53,20 @@ specified, the default selector is used.
 
 .. opt:: Default Goal Selector @toplevel_selector
 
-   This option controls the default selector – used when no selector is
-   specified when applying a tactic – is set to the chosen value. The initial
-   value is 1, hence the tactics are, by default, applied to the first goal.
-   Using value ``all`` will make is so that tactics are, by default, applied to
-   every goal simultaneously. Then, to apply a tactic tac to the first goal
-   only, you can write ``1:tac``. Although more selectors are available, only
-   ``all`` or a single natural number are valid default goal selectors.
+   This option controls the default selector, used when no selector is
+   specified when applying a tactic. The initial value is 1, hence the
+   tactics are, by default, applied to the first goal.
+
+   Using value ``all`` will make it so that tactics are, by default,
+   applied to every goal simultaneously. Then, to apply a tactic tac
+   to the first goal only, you can write ``1:tac``.
+
+   Using value ``!`` enforces that all tactics are used either on a
+   single focused goal or with a local selector (’’strict focusing
+   mode’’).
+
+   Although more selectors are available, only ``all``, ``!`` or a
+   single natural number are valid default goal selectors.
 
 .. _bindingslist:
 
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 0c42a8bb28..a1d7d9b1a7 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -325,6 +325,7 @@ GEXTEND Gram
   ;
   toplevel_selector:
     [ [ sel = selector_body; ":" -> sel
+    |   "!"; ":" -> SelectAlreadyFocused
     |   IDENT "all"; ":" -> SelectAll ] ]
   ;
   tactic_mode:
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 11bb7a2341..bd02d85d59 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -515,6 +515,7 @@ let string_of_genarg_arg (ArgumentType arg) =
     else int i ++ str "-" ++ int j
 
 let pr_goal_selector toplevel = function
+  | SelectAlreadyFocused -> str "!:"
   | SelectNth i -> int i ++ str ":"
   | SelectList l -> prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ str ":"
   | SelectId id -> str "[" ++ Id.print id ++ str "]:"
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 3baa475aba..37abfeee97 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -36,6 +36,7 @@ type letin_flag = bool     (* true = use local def    false = use Leibniz *)
 type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
 
 type goal_selector = Vernacexpr.goal_selector =
+  | SelectAlreadyFocused
   | SelectNth of int
   | SelectList of (int * int) list
   | SelectId of Id.t
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 3baa475aba..37abfeee97 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -36,6 +36,7 @@ type letin_flag = bool     (* true = use local def    false = use Leibniz *)
 type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
 
 type goal_selector = Vernacexpr.goal_selector =
+  | SelectAlreadyFocused
   | SelectNth of int
   | SelectList of (int * int) list
   | SelectId of Id.t
diff --git a/pretyping/vernacexpr.ml b/pretyping/vernacexpr.ml
index 4e1c986f16..548689205a 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
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index abda04ff1b..62a38fa325 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -101,6 +101,18 @@ let solve ?with_end_tac gi info_lvl tac pr =
       | Some _ -> Proofview.Trace.record_info_trace tac
     in
     let tac = match gi with
+      | Vernacexpr.SelectAlreadyFocused ->
+        let open Proofview.Notations in
+        Proofview.numgoals >>= fun n ->
+        if n == 1 then tac
+        else
+          let e = CErrors.UserError
+              (None,
+               Pp.(str "Expected a single focused goal but " ++
+                   int n ++ str " goals are focused."))
+          in
+          Proofview.tclZERO e
+
       | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i tac
       | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l tac
       | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id tac
diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml
index e22d382f7d..d6f7c0e93a 100644
--- a/proofs/proof_bullet.ml
+++ b/proofs/proof_bullet.ml
@@ -212,6 +212,7 @@ let pr_range_selector (i, j) =
   else Pp.(int i ++ str "-" ++ int j)
 
 let pr_goal_selector = function
+  | Vernacexpr.SelectAlreadyFocused -> Pp.str "!"
   | Vernacexpr.SelectAll -> Pp.str "all"
   | Vernacexpr.SelectNth i -> Pp.int i
   | Vernacexpr.SelectList l ->
@@ -221,9 +222,10 @@ let pr_goal_selector = function
   | Vernacexpr.SelectId id -> Names.Id.print id
 
 let parse_goal_selector = function
+  | "!" -> Vernacexpr.SelectAlreadyFocused
   | "all" -> Vernacexpr.SelectAll
   | i ->
-      let err_msg = "The default selector must be \"all\" or a natural number." in
+      let err_msg = "The default selector must be \"all\" or \"!\" or a natural number." in
       begin try
               let i = int_of_string i in
               if i < 0 then CErrors.user_err Pp.(str err_msg);
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 5e81e2d4b1..82b178388e 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -496,7 +496,9 @@ 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")
+    | Vernacexpr.SelectAlreadyFocused ->
+      anomaly ~label:"tclSELECT" Pp.(str "SelectAlreadyFocused not allowed here")
 
   (* Check that holes in arguments have been resolved *)
 
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.