From e262a6262ebb6c3010cb58e96839b0e3d66e09ac Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 11 Apr 2020 17:19:12 -0400
Subject: [proof] Move functions related to `Proof.t` to `Proof`

This makes the API more orthogonal and allows better structure in
future code.
---
 tactics/declare.ml  | 31 ++++---------------------------
 tactics/declare.mli |  6 ------
 2 files changed, 4 insertions(+), 33 deletions(-)

(limited to 'tactics')

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.
-- 
cgit v1.2.3