diff options
| author | coqbot-app[bot] | 2021-03-22 11:29:35 +0000 |
|---|---|---|
| committer | GitHub | 2021-03-22 11:29:35 +0000 |
| commit | dca133d15e39012ae2c7453d93987f500aa2c0fa (patch) | |
| tree | ef90b9cf67f873a90e1a94ba1692f9ed70c2c4b6 | |
| parent | fcfeb5bc45febe1a05f44a0a77b43be6b6905f35 (diff) | |
| parent | b809bf80bed06303f3d5aa2297787782a030f037 (diff) | |
Merge PR #13961: Implement ! goal selector for Ltac2.
Reviewed-by: SkySkimmer
| -rw-r--r-- | test-suite/bugs/closed/bug_13960.v | 10 | ||||
| -rw-r--r-- | user-contrib/Ltac2/tac2entries.ml | 13 |
2 files changed, 22 insertions, 1 deletions
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 |