X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fextlib%2FhExtlib.ml;h=b36a4d89db2630f5d0d192454f706d86fa1054d3;hb=4eeb9c91bd4cea289a808cc494ca7bf8de9ab881;hp=8a0c8cf7d69fb5578d2a851e921d73d5a6546554;hpb=801f0eb3eabe1cbcd66d6a3f52c24eb8f1189611;p=helm.git

diff --git a/components/extlib/hExtlib.ml b/components/extlib/hExtlib.ml
index 8a0c8cf7d..b36a4d89d 100644
--- a/components/extlib/hExtlib.ml
+++ b/components/extlib/hExtlib.ml
@@ -27,7 +27,7 @@
 
 (** PROFILING *)
 
-let profiling_enabled = ComponentsConf.profiling
+let profiling_enabled = false ;; (* ComponentsConf.profiling *)
 
 let something_profiled = ref false
 
@@ -135,6 +135,10 @@ let is_alphanum c = is_alpha c || is_digit c
 
 (** {2 List processing} *)
 
+let flatten_map f l =
+  List.flatten (List.map f l)
+;;
+
 let rec list_uniq ?(eq=(=)) = function 
   | [] -> []
   | h::[] -> [h]
@@ -365,3 +369,7 @@ let raise_localized_exception ~offset floc exn =
    { flocb with Lexing.pos_cnum = x }, { floce with Lexing.pos_cnum = y }
  in
   raise (Localized (floc, exn))
+
+let estimate_size x = 
+  4 * (String.length (Marshal.to_string x [])) / 1024
+