[proof] Deprecate redundant wrappers.

As we would like to reduce the role of proof_global in future
versions, we start to deprecate old compatibility aliases in `Pfedit`
in favor of the real functions underlying the 8.5 proof engine.

We also deprecate a couple of alias types and explicitly mark the few
remaining uses of `Pfedit`.

2 files changed, 119 insertions, 101 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 3fb66d1b8..b28234a50 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -24,19 +24,6 @@ let _ = Goptions.declare_bool_option {
 
 let use_unification_heuristics () = !use_unification_heuristics_ref
 
-let refining = Proof_global.there_are_pending_proofs
-let check_no_pending_proofs = Proof_global.check_no_pending_proof
-
-let get_current_proof_name = Proof_global.get_current_proof_name
-let get_all_proof_names = Proof_global.get_all_proof_names
-
-type lemma_possible_guards = Proof_global.lemma_possible_guards
-type universe_binders = Proof_global.universe_binders
-
-let delete_proof = Proof_global.discard
-let delete_current_proof = Proof_global.discard_current
-let delete_all_proofs = Proof_global.discard_all
-
 let start_proof (id : Id.t) ?pl str sigma hyps c ?init_tac terminator =
   let goals = [ (Global.env_of_context hyps , c) ] in
   Proof_global.start_proof sigma id ?pl str goals terminator;
@@ -55,32 +42,20 @@ let cook_this_proof p =
 let cook_proof () =
   cook_this_proof (fst
     (Proof_global.close_proof ~keep_body_ucst_separate:false (fun x -> x)))
-let get_pftreestate () =
-  Proof_global.give_me_the_proof ()
-
-let set_end_tac tac =
-  Proof_global.set_endline_tactic tac
-
-let set_used_variables l =
-  Proof_global.set_used_variables l
-let get_used_variables () =
-  Proof_global.get_used_variables ()
-
-let get_universe_binders () =
-  Proof_global.get_universe_binders ()
 
 exception NoSuchGoal
 let _ = CErrors.register_handler begin function
   | NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.")
   | _ -> raise CErrors.Unhandled
 end
+
 let get_nth_V82_goal i =
   let p = Proof_global.give_me_the_proof () in
   let { it=goals ; sigma = sigma; } = Proof.V82.subgoals p in
   try
           { it=(List.nth goals (i-1)) ; sigma=sigma; }
   with Failure _ -> raise NoSuchGoal
-    
+
 let get_goal_context_gen i =
   let { it=goal ; sigma=sigma; } =  get_nth_V82_goal i in
   (sigma, Refiner.pf_env { it=goal ; sigma=sigma; })
@@ -106,7 +81,7 @@ let get_current_context () =
     (Evd.from_env env, env)
      | NoSuchGoal ->
         (* No more focused goals ? *)
-        let p = get_pftreestate () in
+        let p = Proof_global.give_me_the_proof () in
         let evd = Proof.in_proof p (fun x -> x) in
         (evd, Global.env ())
 
@@ -165,11 +140,11 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
   try
     let status = by tac in
     let _,(const,univs,_) = cook_proof () in
-    delete_current_proof ();
+    Proof_global.discard_current ();
     const, status, fst univs
   with reraise ->
     let reraise = CErrors.push reraise in
-    delete_current_proof ();
+    Proof_global.discard_current ();
     iraise reraise
 
 let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac =
@@ -257,4 +232,32 @@ let solve_by_implicit_tactic () = match !implicit_tactic with
 | None -> None
 | Some tac -> Some (apply_implicit_tactic tac)
 
+(** Deprecated functions  *)
+let refining = Proof_global.there_are_pending_proofs
+let check_no_pending_proofs = Proof_global.check_no_pending_proof
+
+let get_current_proof_name = Proof_global.get_current_proof_name
+let get_all_proof_names = Proof_global.get_all_proof_names
+
+type lemma_possible_guards = Proof_global.lemma_possible_guards
+type universe_binders = Proof_global.universe_binders
+
+let delete_proof = Proof_global.discard
+let delete_current_proof = Proof_global.discard_current
+let delete_all_proofs = Proof_global.discard_all
+
+let get_pftreestate () =
+  Proof_global.give_me_the_proof ()
+
+let set_end_tac tac =
+  Proof_global.set_endline_tactic tac
+
+let set_used_variables l =
+  Proof_global.set_used_variables l
+
+let get_used_variables () =
+  Proof_global.get_used_variables ()
+
+let get_universe_binders () =
+  Proof_global.get_universe_binders ()
 
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 1bf65b8ae..f009593e9 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -14,39 +14,6 @@ open Term
 open Environ
 open Decl_kinds
 
-(** Several proofs can be opened simultaneously but at most one is
-   focused at some time. The following functions work by side-effect
-   on current set of open proofs. In this module, ``proofs'' means an
-   open proof (something started by vernacular command [Goal], [Lemma]
-   or [Theorem]), and ``goal'' means a subgoal of the current focused
-   proof *)
-
-(** {6 ... } *)
-(** [refining ()] tells if there is some proof in progress, even if a not
-   focused one *)
-
-val refining : unit -> bool
-
-(** [check_no_pending_proofs ()] fails if there is still some proof in
-   progress *)
-
-val check_no_pending_proofs : unit -> unit
-
-(** {6 ... } *)
-(** [delete_proof name] deletes proof of name [name] or fails if no proof
-    has this name *)
-
-val delete_proof : Id.t located -> unit
-
-(** [delete_current_proof ()] deletes current focused proof or fails if
-    no proof is focused *)
-
-val delete_current_proof : unit -> unit
-
-(** [delete_all_proofs ()] deletes all open proofs if any *)
-
-val delete_all_proofs : unit -> unit
-
 (** {6 ... } *)
 (** [start_proof s str env t hook tac] starts a proof of name [s] and
     conclusion [t]; [hook] is optionally a function to be applied at
@@ -55,12 +22,8 @@ val delete_all_proofs : unit -> unit
     systematically apply at initialization time (e.g. to start the
     proof of mutually dependent theorems) *)
 
-type lemma_possible_guards = Proof_global.lemma_possible_guards
-
-type universe_binders = Id.t Loc.located list
-
 val start_proof :
-  Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr ->
+  Id.t -> ?pl:Proof_global.universe_binders -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr ->
   ?init_tac:unit Proofview.tactic ->
   Proof_global.proof_terminator -> unit
 
@@ -80,11 +43,6 @@ val cook_proof : unit ->
     (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind))
 
 (** {6 ... } *)
-(** [get_pftreestate ()] returns the current focused pending proof.
-   @raise NoCurrentProof if there is no pending proof. *)
-
-val get_pftreestate : unit -> Proof.proof
-
 (** [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 *)
@@ -109,34 +67,6 @@ val current_proof_statement :
   unit -> Id.t * goal_kind * EConstr.types
 
 (** {6 ... } *)
-(** [get_current_proof_name ()] return the name of the current focused
-    proof or failed if no proof is focused *)
-
-val get_current_proof_name : unit -> Id.t
-
-(** [get_all_proof_names ()] returns the list of all pending proof names.
-    The first name is the current proof, the other names may come in
-    any order. *)
-
-val get_all_proof_names : unit -> Id.t list
-
-(** {6 ... } *)
-(** [set_end_tac tac] applies tactic [tac] to all subgoal generate
-    by [solve] *)
-
-val set_end_tac : Genarg.glob_generic_argument -> unit
-
-(** {6 ... } *)
-(** [set_used_variables l] declares that section variables [l] will be
-    used in the proof *)
-val set_used_variables :
-  Id.t list -> Context.Named.t * Names.Id.t Loc.located list
-val get_used_variables : unit -> Context.Named.t option
-
-(** {6 Universe binders } *)
-val get_universe_binders : unit -> universe_binders option
-
-(** {6 ... } *)
 (** [solve (SelectNth n) tac] applies tactic [tac] to the [n]th
     subgoal of the current focused proof or raises a [UserError] if no
     proof is focused or if there is no [n]th subgoal. [solve SelectAll
@@ -191,3 +121,88 @@ val clear_implicit_tactic : unit -> unit
 
 (* Raise Exit if cannot solve *)
 val solve_by_implicit_tactic : unit -> Pretyping.inference_hook option
+
+(** {5 Deprecated functions in favor of [Proof_global]} *)
+
+(** {6 ... } *)
+(** Several proofs can be opened simultaneously but at most one is
+   focused at some time. The following functions work by side-effect
+   on current set of open proofs. In this module, ``proofs'' means an
+   open proof (something started by vernacular command [Goal], [Lemma]
+   or [Theorem]), and ``goal'' means a subgoal of the current focused
+   proof *)
+
+(** [refining ()] tells if there is some proof in progress, even if a not
+   focused one *)
+
+val refining : unit -> bool
+[@@ocaml.deprecated "use Proof_global.there_are_pending_proofs"]
+
+(** [check_no_pending_proofs ()] fails if there is still some proof in
+   progress *)
+
+val check_no_pending_proofs : unit -> unit
+[@@ocaml.deprecated "use Proof_global.check_no_pending_proofs"]
+
+(** {6 ... } *)
+(** [delete_proof name] deletes proof of name [name] or fails if no proof
+    has this name *)
+
+val delete_proof : Id.t located -> unit
+[@@ocaml.deprecated "use Proof_global.discard"]
+
+(** [delete_current_proof ()] deletes current focused proof or fails if
+    no proof is focused *)
+
+val delete_current_proof : unit -> unit
+[@@ocaml.deprecated "use Proof_global.discard_current"]
+
+(** [delete_all_proofs ()] deletes all open proofs if any *)
+val delete_all_proofs : unit -> unit
+[@@ocaml.deprecated "use Proof_global.discard_all"]
+
+(** [get_pftreestate ()] returns the current focused pending proof.
+   @raise NoCurrentProof if there is no pending proof. *)
+
+val get_pftreestate : unit -> Proof.proof
+[@@ocaml.deprecated "use Proof_global.give_me_the_proof"]
+
+(** {6 ... } *)
+(** [set_end_tac tac] applies tactic [tac] to all subgoal generate
+    by [solve] *)
+
+val set_end_tac : Genarg.glob_generic_argument -> unit
+[@@ocaml.deprecated "use Proof_global.set_endline_tactic"]
+
+(** {6 ... } *)
+(** [set_used_variables l] declares that section variables [l] will be
+    used in the proof *)
+val set_used_variables :
+  Id.t list -> Context.Named.t * Names.Id.t Loc.located list
+[@@ocaml.deprecated "use Proof_global.set_used_variables"]
+
+val get_used_variables : unit -> Context.Named.t option
+[@@ocaml.deprecated "use Proof_global.get_used_variables"]
+
+(** {6 Universe binders } *)
+val get_universe_binders : unit -> Proof_global.universe_binders option
+[@@ocaml.deprecated "use Proof_global.get_universe_binders"]
+
+(** {6 ... } *)
+(** [get_current_proof_name ()] return the name of the current focused
+    proof or failed if no proof is focused *)
+val get_current_proof_name : unit -> Id.t
+[@@ocaml.deprecated "use Proof_global.get_current_proof_name"]
+
+(** [get_all_proof_names ()] returns the list of all pending proof names.
+    The first name is the current proof, the other names may come in
+    any order. *)
+val get_all_proof_names : unit -> Id.t list
+[@@ocaml.deprecated "use Proof_global.get_all_proof_names"]
+
+type lemma_possible_guards = Proof_global.lemma_possible_guards
+[@@ocaml.deprecated "use Proof_global.lemma_possible_guards"]
+
+type universe_binders = Proof_global.universe_binders
+[@@ocaml.deprecated "use Proof_global.universe_binders"]
+