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

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

2 files changed, 31 insertions, 3 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