[proof] Move functions related to `Proof.t` to `Proof`

This makes the API more orthogonal and allows better structure in
future code.

7 files changed, 40 insertions, 41 deletions

diff --git a/proofs/proof.ml b/proofs/proof.ml
index 731608e629..75aca7e7ff 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -63,7 +63,7 @@ exception CannotUnfocusThisWay
 (* Cannot focus on non-existing subgoals *)
 exception NoSuchGoals of int * int
 
-exception NoSuchGoal of Names.Id.t
+exception NoSuchGoal of Names.Id.t option
 
 exception FullyUnfocused
 
@@ -74,8 +74,10 @@ let _ = CErrors.register_handler begin function
     Some Pp.(str "[Focus] No such goal (" ++ int i ++ str").")
   | NoSuchGoals (i,j) ->
     Some Pp.(str "[Focus] Not every goal in range ["++ int i ++ str","++int j++str"] exist.")
-  | NoSuchGoal id ->
+  | NoSuchGoal (Some id) ->
     Some Pp.(str "[Focus] No such goal: " ++ str (Names.Id.to_string id) ++ str ".")
+  | NoSuchGoal None ->
+    Some Pp.(str "[Focus] No such goal.")
   | FullyUnfocused ->
     Some (Pp.str "The proof is not focused")
   | _ -> None
@@ -233,7 +235,7 @@ let focus_id cond inf id pr =
           raise CannotUnfocusThisWay
      end
   | None ->
-     raise (NoSuchGoal id)
+     raise (NoSuchGoal (Some id))
   end
 
 let rec unfocus kind pr () =
@@ -610,3 +612,20 @@ let refine_by_tactic ~name ~poly env sigma ty tac =
   let neff = neff.Evd.seff_private in
   let (ans, _) = Safe_typing.inline_private_constants env ((ans, Univ.ContextSet.empty), neff) in
   ans, sigma
+
+let get_nth_V82_goal p i =
+  let { sigma; goals } = data p in
+  try { Evd.it = List.nth goals (i-1) ; sigma }
+  with Failure _ -> raise (NoSuchGoal None)
+
+let get_goal_context_gen pf i =
+  let { Evd.it=goal ; sigma=sigma; } = get_nth_V82_goal pf i in
+  (sigma, Global.env_of_context (Goal.V82.hyps sigma goal))
+
+let get_proof_context p =
+  try get_goal_context_gen p 1
+  with
+  | NoSuchGoal _ ->
+    (* No more focused goals *)
+    let { sigma } = data p in
+    sigma, Global.env ()
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 0f327e2a25..0e5bdaf07d 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -143,6 +143,8 @@ exception CannotUnfocusThisWay
    Bullet.push. *)
 exception NoSuchGoals of int * int
 
+exception NoSuchGoal of Names.Id.t option
+
 (* Unfocusing command.
    Raises [FullyUnfocused] if the proof is not focused.
    Raises [CannotUnfocusThisWay] if the proof the unfocusing condition
@@ -238,3 +240,10 @@ val refine_by_tactic
     monad. *)
 
 exception SuggestNoSuchGoals of int * t
+
+(** {6 Helpers to obtain proof state when in an interactive proof } *)
+val get_goal_context_gen : t -> int -> Evd.evar_map * Environ.env
+
+(** [get_proof_context ()] gets the goal context for the first subgoal
+    of the proof *)
+val get_proof_context : t -> Evd.evar_map * Environ.env
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 6945f13fc3..d1b5a852b1 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -864,44 +864,21 @@ let declare_abstract ~name ~poly ~kind ~sign ~secsign ~opaque ~solve_tac sigma c
   let effs = Evd.concat_side_effects eff effs in
   effs, sigma, lem, args, safe
 
-exception NoSuchGoal
-let () = CErrors.register_handler begin function
-  | NoSuchGoal -> Some Pp.(str "No such goal.")
-  | _ -> None
-end
-
-let get_nth_V82_goal p i =
-  let Proof.{ sigma; goals } = Proof.data p in
-  try { Evd.it = List.nth goals (i-1) ; sigma }
-  with Failure _ -> raise NoSuchGoal
-
-let get_goal_context_gen pf i =
-  let { Evd.it=goal ; sigma=sigma; } = get_nth_V82_goal pf i in
-  (sigma, Refiner.pf_env { Evd.it=goal ; sigma=sigma; })
-
 let get_goal_context pf i =
   let p = get_proof pf in
-  get_goal_context_gen p i
+  Proof.get_goal_context_gen p i
 
 let get_current_goal_context pf =
   let p = get_proof pf in
-  try get_goal_context_gen p 1
+  try Proof.get_goal_context_gen p 1
   with
-  | NoSuchGoal ->
+  | Proof.NoSuchGoal _ ->
     (* spiwack: returning empty evar_map, since if there is no goal,
        under focus, there is no accessible evar either. EJGA: this
        seems strange, as we have pf *)
     let env = Global.env () in
     Evd.from_env env, env
 
-let get_proof_context p =
-  try get_goal_context_gen p 1
-  with
-  | NoSuchGoal ->
-    (* No more focused goals *)
-    let { Proof.sigma } = Proof.data p in
-    sigma, Global.env ()
-
 let get_current_context pf =
   let p = get_proof pf in
-  get_proof_context p
+  Proof.get_proof_context p
diff --git a/tactics/declare.mli b/tactics/declare.mli
index ff8a705e60..c50772eeea 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -281,8 +281,6 @@ val build_by_tactic
 
 (** {6 Helpers to obtain proof state when in an interactive proof } *)
 
-exception NoSuchGoal
-
 (** [get_goal_context n] returns the context of the [n]th subgoal of
    the current focused proof or raises a [UserError] if there is no
    focused proof or if there is no more subgoals *)
@@ -292,10 +290,6 @@ val get_goal_context : t -> int -> Evd.evar_map * Environ.env
 (** [get_current_goal_context ()] works as [get_goal_context 1] *)
 val get_current_goal_context : t -> Evd.evar_map * Environ.env
 
-(** [get_proof_context ()] gets the goal context for the first subgoal
-    of the proof *)
-val get_proof_context : Proof.t -> Evd.evar_map * Environ.env
-
 (** [get_current_context ()] returns the context of the
   current focused goal. If there is no focused goal but there
   is a proof in progress, it returns the corresponding evar_map.
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index 9d8e830d64..593d0c7f67 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -136,7 +136,7 @@ h': newdef n <> n
 (use "About" for full details on implicit arguments)
 (use "About" for full details on implicit arguments)
 The command has indeed failed with message:
-No such goal.
+[Focus] No such goal.
 The command has indeed failed with message:
 Query commands only support the single numbered goal selector.
 The command has indeed failed with message:
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 86fd3be4f5..2c5faa4df7 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -375,7 +375,7 @@ let exit_on_error =
    point we should consolidate the code *)
 let show_proof_diff_to_pp pstate =
   let p = Option.get pstate in
-  let sigma, env = Declare.get_proof_context p in
+  let sigma, env = Proof.get_proof_context p in
   let pprf = Proof.partial_proof p in
   Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf
 
@@ -392,7 +392,7 @@ let show_proof_diff_cmd ~state removed =
         let show_removed = Some removed in
         Pp_diff.diff_pp_combined ~tokenize_string ?show_removed o_pp n_pp
       with
-      | Declare.NoSuchGoal
+      | Proof.NoSuchGoal _
       | Option.IsNone -> n_pp
       | Pp_diff.Diff_Failure msg -> begin
           (* todo: print the unparsable string (if we know it) *)
@@ -403,7 +403,7 @@ let show_proof_diff_cmd ~state removed =
     else
       n_pp
   with
-  | Declare.NoSuchGoal
+  | Proof.NoSuchGoal _
   | Option.IsNone ->
     CErrors.user_err (str "No goals to show.")
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 37808a3726..860671aed7 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -100,7 +100,7 @@ let show_proof ~pstate =
     Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf
   (* We print nothing if there are no goals left *)
   with
-  | Declare.NoSuchGoal
+  | Proof.NoSuchGoal _
   | Option.IsNone ->
     user_err (str "No goals to show.")