diff options
| -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 |