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 /vernac/himsg.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 'vernac/himsg.mli')
| -rw-r--r-- | vernac/himsg.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/himsg.mli b/vernac/himsg.mli index 5b91f9e68..8945ebadb 100644 --- a/vernac/himsg.mli +++ b/vernac/himsg.mli @@ -27,7 +27,7 @@ val explain_typeclass_error : env -> typeclass_error -> Pp.t val explain_recursion_scheme_error : recursion_scheme_error -> Pp.t -val explain_refiner_error : refiner_error -> Pp.t +val explain_refiner_error : env -> Evd.evar_map -> refiner_error -> Pp.t val explain_pattern_matching_error : env -> Evd.evar_map -> pattern_matching_error -> Pp.t |