[tactics] Remove dependency of abstract on global proof state.

In order to do so we place the polymorphic status and name in the
read-only part of the monad.

Note the added comments, as well as the fact that almost no part of
tactics depends on `proofs` nor `interp`, thus they should be placed
just after pretyping.

Gaëtan Gilbert noted that ideally, abstract should not depend on the
polymorphic status, should we be able to defer closing of the
constant, however this will require significant effort.

Also, we may deprecate nameless abstract, thus rending both of the
changes this PR need unnecessary.

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