diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-19 19:08:35 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-21 18:04:32 +0100 |
| commit | 0ddf7d9c35eb2dd5f368e7a5735970ef1fd41fc6 (patch) | |
| tree | 0bc32293ac19ddd63cf764ccbd224b086c7836bc /tactics/hints.mli | |
| parent | b75beb248873db7d9ab8e4a078022b2ed0edcd36 (diff) | |
[printing] Deprecate all printing functions accessing the global proof.
We'd like to handle proofs functionally we thus recommend not to use
printing functions without an explicit context.
We also adapt most of the code, making more explicit where the
printing environment is coming from.
An open task is to refactor some code so we gradually make the
`Pfedit.get_current_context ()` disappear.
Diffstat (limited to 'tactics/hints.mli')
| -rw-r--r-- | tactics/hints.mli | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/tactics/hints.mli b/tactics/hints.mli index 22df29b80..cbf204981 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -260,14 +260,15 @@ val rewrite_db : hint_db_name (** Printing hints *) -val pr_searchtable : unit -> Pp.t +val pr_searchtable : env -> evar_map -> Pp.t val pr_applicable_hint : unit -> Pp.t -val pr_hint_ref : global_reference -> Pp.t -val pr_hint_db_by_name : hint_db_name -> Pp.t +val pr_hint_ref : env -> evar_map -> global_reference -> 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 val pr_hint_db : Hint_db.t -> Pp.t -val pr_hint : hint -> Pp.t +[@@ocaml.deprecated "please used pr_hint_db_env"] +val pr_hint : env -> evar_map -> hint -> Pp.t (** Hook for changing the initialization of auto *) - val add_hints_init : (unit -> unit) -> unit |