1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
18
let memory_stat = ref false
20
let print_memory_stat () =
21
if !memory_stat then begin
22
Format.printf "total heap size = %d kbytes\n" (heap_size_kb ());
23
Format.print_newline();
27
let output_context = ref false
29
let pr_engt = function
30
Some ImpredicativeSet ->
31
str "Theory: Set is impredicative"
33
str "Theory: Set is predicative"
35
let cst_filter f csts =
37
(fun c ce acc -> if f c ce then c::acc else acc)
40
let is_ax _ cb = cb.const_body = None
43
let axs = cst_filter is_ax csts in
47
hv 2 (str "Axioms:" ++ fnl() ++ prlist_with_sep fnl Indtypes.prcon axs)
49
let print_context env =
50
if !output_context then begin
53
{env_constants=csts; env_inductives=inds;
54
env_modules=mods; env_modtypes=mtys};
56
{env_universes=univ; env_engagement=engt}} = env in
58
(fnl() ++ str"CONTEXT SUMMARY" ++ fnl() ++
59
str"===============" ++ fnl() ++ fnl() ++
60
str "* " ++ hov 0 (pr_engt engt ++ fnl()) ++ fnl() ++
61
str "* " ++ hov 0 (pr_ax csts) ++
66
print_context (Safe_typing.get_env());