From 0ba10d800ae221377bf76dc1e5f5b4351a95cf42 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 26 Aug 2009 12:57:11 +0000
Subject: Coloringaux: make identifiers unique; special treatment of precolored
   nodes a la Appel and George. Maps: in PTree.combine, compress useless
 subtrees. Lattice: more efficient implementation of LPMap. Makefile: build
 profiling version

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1139 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 lib/Camlcoq.ml | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'lib/Camlcoq.ml')

diff --git a/lib/Camlcoq.ml b/lib/Camlcoq.ml
index c7abdccd..436583f1 100644
--- a/lib/Camlcoq.ml
+++ b/lib/Camlcoq.ml
@@ -127,3 +127,13 @@ let print_timers () =
 
 let _ = at_exit print_timers
 *)
+
+(* Heap profiling facility *)
+
+(*
+let heap_info msg =
+  Gc.full_major();
+  let s = Gc.stat() in
+  Printf.printf "%s: size %d live %d\n " msg s.Gc.heap_words s.Gc.live_words;
+  flush stdout
+*)
-- 
cgit