aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqtop.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-11-19 19:08:35 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-11-21 18:04:32 +0100
commit0ddf7d9c35eb2dd5f368e7a5735970ef1fd41fc6 (patch)
tree0bc32293ac19ddd63cf764ccbd224b086c7836bc /toplevel/coqtop.ml
parentb75beb248873db7d9ab8e4a078022b2ed0edcd36 (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 'toplevel/coqtop.ml')
-rw-r--r--toplevel/coqtop.ml6
1 files changed, 4 insertions, 2 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index f3d5d9b85..c61a1fd41 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -844,8 +844,10 @@ let start () =
exit 1
| _ ->
flush_all();
- if !output_context then
- Feedback.msg_notice Flags.(with_option raw_print Prettyp.print_full_pure_context () ++ fnl ());
+ if !output_context then begin
+ let sigma, env = Pfedit.get_current_context () in
+ Feedback.msg_notice (Flags.(with_option raw_print (Prettyp.print_full_pure_context env) sigma) ++ fnl ())
+ end;
Profile.print_profile ();
exit 0