diff options
Diffstat (limited to 'user-contrib')
| -rw-r--r-- | user-contrib/Ltac2/tac2entries.ml | 21 |
1 files changed, 4 insertions, 17 deletions
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index faa1e74728..5ddf56402f 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -811,24 +811,11 @@ let perform_eval ~pstate e = Goal_select.get_default_goal_selector (), Declare.Proof.get pstate in - let v = match selector with - | Goal_select.SelectNth i -> Proofview.tclFOCUS i i v - | Goal_select.SelectList l -> Proofview.tclFOCUSLIST l v - | Goal_select.SelectId id -> Proofview.tclFOCUSID id v - | Goal_select.SelectAll -> v - | 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 + let nosuchgoal = + let info = Exninfo.reify () in + Proofview.tclZERO ~info (Proof.SuggestNoSuchGoals (1,proof)) in + let v = Goal_select.tclSELECT ~nosuchgoal selector v in let (proof, _, ans) = Proof.run_tactic (Global.env ()) v proof in let { Proof.sigma } = Proof.data proof in let name = int_name () in |