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 "!".
---
 test-suite/bugs/closed/bug_13960.v | 10 ++++++++++
 user-contrib/Ltac2/tac2entries.ml  | 13 ++++++++++++-
 2 files changed, 22 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/bug_13960.v

diff --git a/test-suite/bugs/closed/bug_13960.v b/test-suite/bugs/closed/bug_13960.v
new file mode 100644
index 0000000000..947db9586f
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13960.v
@@ -0,0 +1,10 @@
+Require Ltac2.Ltac2.
+
+Set Default Goal Selector "!".
+
+Ltac2 t () := let _ := Message.print (Message.of_string "hi") in 42.
+
+Goal False.
+Proof.
+Ltac2 Eval t ().
+Abort.
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