From 7fd23f30ef6c52aabc8d1084171d906e1080f3f2 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 24 Apr 2019 13:56:25 +0200
Subject: Fix proof bullet error helper (nosuchgoal)

The [int] is incorrect for list focusing, we could work a bit harder
to fix that. It's only used for pluralisation in the error message "no
such goal(s)" so we could also ignore the issue.
---
 proofs/pfedit.ml       | 16 +++++-----------
 proofs/proof_global.ml |  7 -------
 2 files changed, 5 insertions(+), 18 deletions(-)

(limited to 'proofs')

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index da3bd41bda..4f36354f79 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -65,13 +65,6 @@ let get_current_context pf =
     let evd = Proof.in_proof p (fun x -> x) in
     evd, Global.env ()
 
-(* Improved error messages *)
-let run_tactic env tac pr =
-  try Proof.run_tactic env tac pr
-  with
-  | Proofview.NoSuchGoals i ->
-    raise Proof_bullet.(SuggestNoSuchGoals(i,pr))
-
 let solve ?with_end_tac gi info_lvl tac pr =
     let tac = match with_end_tac with
       | None -> tac
@@ -80,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
@@ -93,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 =
@@ -104,7 +98,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
       else tac
     in
     let env = Global.env () in
-    let (p,(status,info)) = run_tactic env tac pr in
+    let (p,(status,info)) = Proof.run_tactic env tac pr in
     let env = Global.env () in
     let sigma = Evd.from_env env in
     let () =
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 5b77b97988..08b98d702a 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -94,13 +94,6 @@ let with_current_proof f (ps, psl) =
   let ps = { ps with proof = newpr } in
   (ps, psl), ret
 
-(* Improved error messages *)
-let with_current_proof f ((ps,_) as pf) =
-  try with_current_proof f pf
-  with
-  | Proofview.NoSuchGoals i ->
-    raise Proof_bullet.(SuggestNoSuchGoals(i,ps.proof))
-
 let simple_with_current_proof f pf =
   let p, () = with_current_proof (fun t p -> f t p , ()) pf in p
 
-- 
cgit v1.2.3