From f610068823b33bdc0af752a646df05b98489d7ce Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 11 Jun 2017 06:08:02 +0200
Subject: [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`.
---
 tactics/hints.ml   |  3 +--
 tactics/tactics.ml | 11 +++++------
 2 files changed, 6 insertions(+), 8 deletions(-)

(limited to 'tactics')

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 773abb9f0c..681db5d08e 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -29,7 +29,6 @@ open Decl_kinds
 open Pattern
 open Patternops
 open Clenv
-open Pfedit
 open Tacred
 open Printer
 open Vernacexpr
@@ -1462,7 +1461,7 @@ let pr_hint_term sigma cl =
 
 (* print all hints that apply to the concl of the current goal *)
 let pr_applicable_hint () =
-  let pts = get_pftreestate () in
+  let pts = Proof_global.give_me_the_proof () in
   let glss = Proof.V82.subgoals pts in
   match glss.Evd.it with
   | [] -> CErrors.user_err Pp.(str "No focused goal.")
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b553f316c2..7e560b1762 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -25,7 +25,6 @@ open Inductiveops
 open Reductionops
 open Globnames
 open Evd
-open Pfedit
 open Tacred
 open Genredexpr
 open Tacmach.New
@@ -543,7 +542,7 @@ end
 let fix ido n = match ido with
   | None ->
     Proofview.Goal.enter begin fun gl ->
-      let name = Pfedit.get_current_proof_name () in
+      let name = Proof_global.get_current_proof_name () in
       let id = new_fresh_id [] name gl in
       mutual_fix id n [] 0
     end
@@ -594,7 +593,7 @@ end
 let cofix ido = match ido with
   | None ->
     Proofview.Goal.enter begin fun gl ->
-      let name = Pfedit.get_current_proof_name () in
+      let name = Proof_global.get_current_proof_name () in
       let id = new_fresh_id [] name gl in
       mutual_cofix id [] 0
     end
@@ -1140,7 +1139,7 @@ let rec intros_move = function
 let tactic_infer_flags with_evar = {
   Pretyping.use_typeclasses = true;
   Pretyping.solve_unification_constraints = true;
-  Pretyping.use_hook = solve_by_implicit_tactic ();
+  Pretyping.use_hook = Pfedit.solve_by_implicit_tactic ();
   Pretyping.fail_evar = not with_evar;
   Pretyping.expand_evars = true }
 
@@ -5032,11 +5031,11 @@ let name_op_to_name name_op object_kind suffix =
   let default_gk = (Global, false, object_kind) in
   match name_op with
     | Some s ->
-      (try let _, gk, _ = current_proof_statement () in s, gk
+      (try let _, gk, _ = Pfedit.current_proof_statement () in s, gk
        with NoCurrentProof -> s, default_gk)
     | None   ->
       let name, gk =
-	try let name, gk, _ = current_proof_statement () in name, gk
+	try let name, gk, _ = Pfedit.current_proof_statement () in name, gk
 	with NoCurrentProof -> anon_id, default_gk in
       add_suffix name suffix, gk
 
-- 
cgit v1.2.3