diff options
Diffstat (limited to 'checker/check_stat.ml')
| -rw-r--r-- | checker/check_stat.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/checker/check_stat.ml b/checker/check_stat.ml index 84f5684d4..a26c93a30 100644 --- a/checker/check_stat.ml +++ b/checker/check_stat.ml @@ -57,12 +57,13 @@ let print_context env = env_modules=mods; env_modtypes=mtys}; env_stratification= {env_universes=univ; env_engagement=engt}} = env in - ppnl(hov 0 + Feedback.msg_notice + (hov 0 (fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++ str"===============" ++ fnl() ++ fnl() ++ str "* " ++ hov 0 (pr_engagement engt ++ fnl()) ++ fnl() ++ str "* " ++ hov 0 (pr_ax csts) ++ - fnl())); pp_flush() + fnl())); end let stats () = |