diff options
| author | Emilio Jesus Gallego Arias | 2017-11-19 19:08:35 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-11-21 18:04:32 +0100 |
| commit | 0ddf7d9c35eb2dd5f368e7a5735970ef1fd41fc6 (patch) | |
| tree | 0bc32293ac19ddd63cf764ccbd224b086c7836bc /toplevel | |
| 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 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 6 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 4 |
2 files changed, 7 insertions, 3 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index f3d5d9b859..c61a1fd418 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 diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index cf63fbdc3d..8fdaedbaf7 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -100,7 +100,9 @@ let print_cmd_header ?loc com = Format.pp_print_flush !Topfmt.std_ft () let pr_open_cur_subgoals () = - try Printer.pr_open_subgoals () + try + let proof = Proof_global.give_me_the_proof () in + Printer.pr_open_subgoals ~proof with Proof_global.NoCurrentProof -> Pp.str "" (* Reenable when we get back to feedback printing *) |