4 files changed, 18 insertions, 18 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index ef4a74b273..4f36354f79 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -73,6 +73,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
       | None -> tac
       | Some _ -> Proofview.Trace.record_info_trace tac
     in
+    let nosuchgoal = Proofview.tclZERO (Proof_bullet.SuggestNoSuchGoals (1,pr)) in
     let tac = let open Goal_select in match gi with
       | SelectAlreadyFocused ->
         let open Proofview.Notations in
@@ -86,9 +87,9 @@ let solve ?with_end_tac gi info_lvl tac pr =
           in
           Proofview.tclZERO e
 
-      | SelectNth i -> Proofview.tclFOCUS i i tac
-      | SelectList l -> Proofview.tclFOCUSLIST l tac
-      | SelectId id -> Proofview.tclFOCUSID id tac
+      | SelectNth i -> Proofview.tclFOCUS ~nosuchgoal i i tac
+      | SelectList l -> Proofview.tclFOCUSLIST ~nosuchgoal l tac
+      | SelectId id -> Proofview.tclFOCUSID ~nosuchgoal id tac
       | SelectAll -> tac
     in
     let tac =
diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml
index 2ca4f0afb4..640feb2f5b 100644
--- a/proofs/proof_bullet.ml
+++ b/proofs/proof_bullet.ml
@@ -197,3 +197,15 @@ let put p b =
 
 let suggest p =
   (!current_behavior).suggest p
+
+(* Better printing for bullet exceptions *)
+exception SuggestNoSuchGoals of int * Proof.t
+
+let _ = CErrors.register_handler begin function
+    | SuggestNoSuchGoals(n,proof) ->
+      let suffix = suggest proof in
+      CErrors.user_err
+        Pp.(str "No such " ++ str (CString.plural n "goal") ++ str "." ++
+            pr_non_empty_arg (fun x -> x) suffix)
+    | _ -> raise CErrors.Unhandled
+  end
diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli
index 0fcc647a6f..6fdf818497 100644
--- a/proofs/proof_bullet.mli
+++ b/proofs/proof_bullet.mli
@@ -44,3 +44,5 @@ val register_behavior : behavior -> unit
      *)
 val put : Proof.t -> t -> Proof.t
 val suggest : Proof.t -> Pp.t
+
+exception SuggestNoSuchGoals of int * Proof.t
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 86d3d9601e..08b98d702a 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -348,18 +348,3 @@ let update_global_env (pf : t) =
        let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac p in
          (p, ()))) pf
   in res
-
-(* XXX: This hook is used to provide a better error w.r.t. bullets,
-   however the proof engine [surprise!] knows nothing about bullets so
-   here we have a layering violation. The right fix is to modify the
-   entry point to handle this and reraise the exception with the
-   needed information. *)
-(* let _ =
- *   let hook n =
- *     try
- *       let prf = give_me_the_proof pf in
- *       (Proof_bullet.suggest prf)
- *     with NoCurrentProof -> mt ()
- *   in
- *   Proofview.set_nosuchgoals_hook hook *)
-