summaryrefslogtreecommitdiff
path: root/checker/check_stat.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /checker/check_stat.ml
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'checker/check_stat.ml')
-rw-r--r--checker/check_stat.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index 6ea153a3..170ac638 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -17,7 +17,7 @@ open Environ
let memory_stat = ref false
-let print_memory_stat () =
+let print_memory_stat () =
if !memory_stat then begin
Format.printf "total heap size = %d kbytes\n" (heap_size_kb ());
Format.print_newline();
@@ -33,11 +33,11 @@ let pr_engt = function
str "Theory: Set is predicative"
let cst_filter f csts =
- Cmap.fold
+ Cmap_env.fold
(fun c ce acc -> if f c ce then c::acc else acc)
csts []
-let is_ax _ cb = cb.const_body = None
+let is_ax _ cb = cb.const_body = None
let pr_ax csts =
let axs = cst_filter is_ax csts in