From 54a2a3a07e14c597b264566e01d2ecc69c4bd90c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 8 Apr 2018 03:51:00 +0200
Subject: [tactic] Adapt tactic layer to removal of imperative proof state.

State in `Proof_global` was mostly used for debugging, so not a big
change.
---
 tactics/class_tactics.ml | 11 ++++++-----
 tactics/hints.ml         |  4 ++--
 tactics/hints.mli        |  2 +-
 3 files changed, 9 insertions(+), 8 deletions(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index a3620f4081..44102afd74 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -933,11 +933,12 @@ module Search = struct
        try
          (* Instance may try to call this before a proof is set up!
             Thus, give_me_the_proof will fail. Beware! *)
-         let name, poly = try
-             let Proof.{ name; poly } = Proof.data Proof_global.(give_me_the_proof ()) in
-             name, poly
-           with | Proof_global.NoCurrentProof ->
-             Id.of_string "instance", false
+         let name, poly =
+           (* try
+            *   let Proof.{ name; poly } = Proof.data Proof_global.(give_me_the_proof ()) in
+            *   name, poly
+            * with | Proof_global.NoCurrentProof -> *)
+           Id.of_string "instance", false
          in
          let (), pv', (unsafe, shelved, gaveup), _ =
            Proofview.apply ~name ~poly env tac pv
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 85d75f1010..3a7e67cb3f 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1514,9 +1514,9 @@ let pr_hint_term env sigma cl =
     (str "No hint applicable for current goal")
 
 (* print all hints that apply to the concl of the current goal *)
-let pr_applicable_hint () =
+let pr_applicable_hint pf =
   let env = Global.env () in
-  let pts = Proof_global.give_me_the_proof () in
+  let pts = Proof_global.give_me_the_proof pf in
   let Proof.{goals;sigma} = Proof.data pts in
   match goals with
   | [] -> CErrors.user_err Pp.(str "No focused goal.")
diff --git a/tactics/hints.mli b/tactics/hints.mli
index dd2c63d351..e84e423faa 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -294,7 +294,7 @@ val wrap_hint_warning_fun : env -> evar_map ->
 (** Printing  hints *)
 
 val pr_searchtable : env -> evar_map -> Pp.t
-val pr_applicable_hint : unit -> Pp.t
+val pr_applicable_hint : Proof_global.t -> Pp.t
 val pr_hint_ref : env -> evar_map -> GlobRef.t -> Pp.t
 val pr_hint_db_by_name : env -> evar_map -> hint_db_name -> Pp.t
 val pr_hint_db_env : env -> evar_map -> Hint_db.t -> Pp.t
-- 
cgit v1.2.3