diff options
Diffstat (limited to 'toplevel/coqtop.ml')
| -rw-r--r-- | toplevel/coqtop.ml | 6 |
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 |