5 files changed, 6 insertions, 34 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 7f1ae6d12b..9509c36ec0 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -70,11 +70,6 @@ let get_current_context ?p () =
         let evd = Proof.in_proof p (fun x -> x) in
         (evd, Global.env ())
 
-let current_proof_statement () =
-  match Proof_global.V82.get_current_initial_conclusions () with
-    | (id,([concl],strength)) -> id,strength,concl
-    | _ -> CErrors.anomaly ~label:"Pfedit.current_proof_statement" (Pp.str "more than one statement.")
-
 let solve ?with_end_tac gi info_lvl tac pr =
   try 
     let tac = match with_end_tac with
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 5699320af5..29ab00876a 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -34,11 +34,6 @@ val get_current_goal_context : unit -> Evd.evar_map * env
 
 val get_current_context : ?p:Proof.t -> unit -> Evd.evar_map * env
 
-(** [current_proof_statement] *)
-
-val current_proof_statement :
-  unit -> Id.t * goal_kind * EConstr.types
-
 (** {6 ... } *)
 
 (** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 4ce932b93d..e40940f652 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -415,8 +415,9 @@ let run_tactic env tac pr =
     Proofview.Unsafe.tclEVARS sigma >>= fun () ->
     Proofview.tclUNIT retrieved
   in
+  let { name; poly } = pr in
   let (retrieved,proofview,(status,to_shelve,give_up),info_trace) =
-    Proofview.apply env tac sp
+    Proofview.apply ~name ~poly env tac sp
   in
   let sigma = Proofview.return proofview in
   let to_shelve = undef sigma to_shelve in
@@ -498,7 +499,8 @@ module V82 = struct
       let sigma = Evar_refiner.w_refine (evk, evi) (ltac_vars, rawc) sigma in
       Proofview.Unsafe.tclEVARS sigma
     end in
-    let ((), proofview, _, _) = Proofview.apply env tac pr.proofview in
+    let { name; poly } = pr in
+    let ((), proofview, _, _) = Proofview.apply ~name ~poly env tac pr.proofview in
     let shelf =
       List.filter begin fun g ->
         Evd.is_undefined (Proofview.return proofview) g
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 9ee9e7ae2c..0cfc010c1a 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -66,12 +66,6 @@ let pstates = ref ([] : pstate list)
 (* combinators for the current_proof lists *)
 let push a l = l := a::!l
 
-exception NoSuchProof
-let () = CErrors.register_handler begin function
-  | NoSuchProof -> CErrors.user_err Pp.(str "No such proof.")
-  | _ -> raise CErrors.Unhandled
-end
-
 exception NoCurrentProof
 let () = CErrors.register_handler begin function
   | NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof (No proof-editing in progress).")
@@ -91,6 +85,7 @@ let cur_pstate () =
 let give_me_the_proof () = (cur_pstate ()).proof
 let give_me_the_proof_opt () = try Some (give_me_the_proof ()) with | NoCurrentProof -> None
 let get_current_proof_name () = (Proof.data (cur_pstate ()).proof).Proof.name
+let get_current_persistence () = (cur_pstate ()).strength
 
 let with_current_proof f =
   match !pstates with
@@ -386,15 +381,6 @@ let set_terminator hook =
   | [] -> raise NoCurrentProof
   | p :: ps -> pstates := { p with terminator = CEphemeron.create hook } :: ps
 
-module V82 = struct
-  let get_current_initial_conclusions () =
-  let { proof; strength } = cur_pstate () in
-  let Proof.{ name; entry } = Proof.data proof in
-  let initial = Proofview.initial_goals entry in
-  let goals = List.map (fun (o, c) -> c) initial in
-  name, (goals, strength)
-end
-
 let freeze ~marshallable =
   if marshallable then CErrors.anomaly (Pp.str"full marshalling of proof state not supported.")
   else !pstates
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 40920f51a3..38e234eaee 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -17,6 +17,7 @@ val there_are_pending_proofs : unit -> bool
 val check_no_pending_proof : unit -> unit
 
 val get_current_proof_name : unit -> Names.Id.t
+val get_current_persistence : unit -> Decl_kinds.goal_kind
 val get_all_proof_names : unit -> Names.Id.t list
 
 val discard : Names.lident -> unit
@@ -104,8 +105,6 @@ val close_future_proof : opaque:opacity_flag -> feedback_id:Stateid.t ->
 val get_terminator : unit -> proof_terminator
 val set_terminator : proof_terminator -> unit
 
-exception NoSuchProof
-
 val get_open_goals : unit -> int
 
 (** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is
@@ -129,11 +128,6 @@ val get_used_variables : unit -> Constr.named_context option
 (** Get the universe declaration associated to the current proof. *)
 val get_universe_decl : unit -> UState.universe_decl
 
-module V82 : sig
-  val get_current_initial_conclusions : unit -> Names.Id.t *(EConstr.types list *
-  Decl_kinds.goal_kind)
-end
-
 val freeze : marshallable:bool -> t
 val unfreeze : t -> unit
 val proof_of_state : t -> Proof.t