X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fcommon%2Foutput.ml;h=c2e43d460a2e5dc1ecc278c9b325089dbd302810;hb=ea41b1f6e212334924a8de4b2ff53b2586de9c4b;hp=6dd526bfb71cc88dd9ecce3e1fb2f13ba533cc94;hpb=01304bffd3ee2a66216214a9e1a8ee7fdfdf16e3;p=helm.git

diff --git a/helm/software/lambda-delta/common/output.ml b/helm/software/lambda-delta/common/output.ml
index 6dd526bfb..c2e43d460 100644
--- 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