some interfaces improved

[helm.git] / helm / software / lambda-delta / common / output.ml

diff --git a/helm/software/lambda-delta/common/output.ml b/helm/software/lambda-delta/common/output.ml
index 6dd526bfb71cc88dd9ecce3e1fb2f13ba533cc94..c2e43d460a2e5dc1ecc278c9b325089dbd302810 100644 (file)
--- a/helm/software/lambda-delta/common/output.ml
+++ b/helm/software/lambda-delta/common/output.ml
@@ -12,6 +12,8 @@
 module P = Printf
 module L = Log
 
+let icm = ref 0
+
 type reductions = {
    beta   : int;
    zeta   : int;
@@ -67,6 +69,7 @@ let print_reductions () =
    L.warn (P.sprintf "      Reference typing:       %7u" rt);
    L.warn (P.sprintf "        Local:                %7u" r.lrt);
    L.warn (P.sprintf "        Global:               %7u" r.grt);
-   L.warn (P.sprintf "      Sort inclusion:         %7u" r.si)
+   L.warn (P.sprintf "      Sort inclusion:         %7u" r.si);
+   L.warn (P.sprintf "  Relocated nodes (icm):      %7u" !icm)
 
 let indexes = ref false