From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 27 Dec 2016 16:53:30 +0100 Subject: Imported Upstream version 8.6 --- checker/check_stat.ml | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) (limited to 'checker/check_stat.ml') 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 () = -- cgit v1.2.3