diff options
| author | Emilio Jesus Gallego Arias | 2018-04-08 03:51:00 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-27 23:22:50 +0100 |
| commit | 54a2a3a07e14c597b264566e01d2ecc69c4bd90c (patch) | |
| tree | 52defd39c09a3f981859e053e80946b5495c2039 | |
| parent | 3b95c063fae710bc7a943e0dd02617bac09c21bc (diff) | |
[tactic] Adapt tactic layer to removal of imperative proof state.
State in `Proof_global` was mostly used for debugging, so not a big
change.
| -rw-r--r-- | tactics/class_tactics.ml | 11 | ||||
| -rw-r--r-- | tactics/hints.ml | 4 | ||||
| -rw-r--r-- | tactics/hints.mli | 2 |
3 files changed, 9 insertions, 8 deletions
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 |