From b809bf80bed06303f3d5aa2297787782a030f037 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 18 Mar 2021 22:21:19 +0100
Subject: Implement ! goal selector for Ltac2.

Fixes #13960: Ltac2 Eval does not work with Set Default Goal Selector "!".
---
 user-contrib/Ltac2/tac2entries.ml | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

(limited to 'user-contrib')

diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index d0655890a7..faa1e74728 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -816,7 +816,18 @@ let perform_eval ~pstate e =
   | Goal_select.SelectList l -> Proofview.tclFOCUSLIST l v
   | Goal_select.SelectId id -> Proofview.tclFOCUSID id v
   | Goal_select.SelectAll -> v
-  | Goal_select.SelectAlreadyFocused -> assert false (* TODO **)
+  | Goal_select.SelectAlreadyFocused ->
+    let open Proofview.Notations in
+    Proofview.numgoals >>= fun n ->
+    if Int.equal n 1 then v
+    else
+      let e = CErrors.UserError
+          (None,
+            Pp.(str "Expected a single focused goal but " ++
+                int n ++ str " goals are focused."))
+      in
+      let info = Exninfo.reify () in
+      Proofview.tclZERO ~info e
   in
   let (proof, _, ans) = Proof.run_tactic (Global.env ()) v proof in
   let { Proof.sigma } = Proof.data proof in
-- 
cgit v1.2.3