diff options
Diffstat (limited to 'checker/check_stat.ml')
| -rw-r--r-- | checker/check_stat.ml | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/checker/check_stat.ml b/checker/check_stat.ml index 05a2a1b9..d041f1b7 100644 --- a/checker/check_stat.ml +++ b/checker/check_stat.ml @@ -23,11 +23,17 @@ let print_memory_stat () = let output_context = ref false -let pr_engt = function - Some ImpredicativeSet -> - str "Theory: Set is impredicative" - | None -> - str "Theory: Set is predicative" +let pr_engagement (impr_set,type_in_type) = + 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 = Cmap_env.fold @@ -54,7 +60,7 @@ let print_context env = ppnl(hov 0 (fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++ str"===============" ++ fnl() ++ fnl() ++ - str "* " ++ hov 0 (pr_engt engt ++ fnl()) ++ fnl() ++ + str "* " ++ hov 0 (pr_engagement engt ++ fnl()) ++ fnl() ++ str "* " ++ hov 0 (pr_ax csts) ++ fnl())); pp_flush() end |