diff options
author | 2016-12-27 16:53:30 +0100 | |
---|---|---|
committer | 2016-12-27 18:33:25 +0100 | |
commit | 1b92c226e563643da187b8614d5888dc4855eb43 (patch) | |
tree | c4c3d204b36468b58cb71050ba95f06b8dd7bc2e /checker/check_stat.ml | |
parent | 7c9b0a702976078b813e6493c1284af62a3f093c (diff) |
Imported Upstream version 8.6
Diffstat (limited to 'checker/check_stat.ml')
-rw-r--r-- | checker/check_stat.ml | 15 |
1 files changed, 5 insertions, 10 deletions
diff --git a/checker/check_stat.ml b/checker/check_stat.ml index d031975d..741f5328 100644 --- a/checker/check_stat.ml +++ b/checker/check_stat.ml @@ -18,21 +18,16 @@ let print_memory_stat () = if !memory_stat then begin Format.printf "total heap size = %d kbytes\n" (CObj.heap_size_kb ()); Format.print_newline(); - flush_all() + Format.print_flush() end let output_context = ref false -let pr_engagement (impr_set,type_in_type) = +let pr_engagement impr_set = begin match impr_set with | ImpredicativeSet -> str "Theory: Set is impredicative" | PredicativeSet -> str "Theory: Set is predicative" - end ++ - begin - match type_in_type with - | StratifiedType -> str "Theory: Stratified type hierarchy" - | TypeInType -> str "Theory: Type is of type Type" end let cst_filter f csts = @@ -57,12 +52,12 @@ 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() + str "* " ++ hov 0 (pr_ax csts))); end let stats () = |