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/btauto/refl_btauto.ml | |
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/btauto/refl_btauto.ml')
-rw-r--r-- | plugins/btauto/refl_btauto.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml index da8955f0d..a09abfa19 100644 --- a/plugins/btauto/refl_btauto.ml +++ b/plugins/btauto/refl_btauto.ml @@ -200,7 +200,8 @@ module Btauto = struct let assign = List.combine env var in let map_msg (key, v) = let b = if v then str "true" else str "false" in - let term = Printer.pr_constr key in + let sigma, env = Pfedit.get_current_context () in + let term = Printer.pr_constr_env env sigma key in term ++ spc () ++ str ":=" ++ spc () ++ b in let assign = List.map map_msg assign in |