diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-07-10 01:13:59 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-07-10 19:18:41 +0200 |
| commit | 9c732a5c878bac2592cb397aca3d17cfefdcd023 (patch) | |
| tree | 7defb39c88bdf0d163ca323955d11f1a50d2367d /checker/check_stat.ml | |
| parent | 591e7e484d544e958595a0fb784336ae050a9c74 (diff) | |
Option -type-in-type: added support in checker and making it contaminating
in vo files (this was not done yet in 24d0027f0 and 090fffa57b).
Reused field "engagement" to carry information about both
impredicativity of set and type in type.
For the record: maybe some further checks to do around the sort of the
inductive types in coqchk?
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 05a2a1b99..d041f1b7e 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 |