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 /plugins/ssr/ssrparser.ml4 | |
| 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 'plugins/ssr/ssrparser.ml4')
| -rw-r--r-- | plugins/ssr/ssrparser.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 7b591fead..46403aef3 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -1131,7 +1131,7 @@ let pr_fwd_guarded prval prval' = function | (fk, h), (_, (_, Some c)) -> pr_gen_fwd prval pr_constr_expr prl_constr_expr fk (format_constr_expr h c) | (fk, h), (_, (c, None)) -> - pr_gen_fwd prval' pr_glob_constr prl_glob_constr fk (format_glob_constr h c) + pr_gen_fwd prval' pr_glob_constr_env prl_glob_constr fk (format_glob_constr h c) let pr_unguarded prc prlc = prlc |