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

diff --git a/helm/software/lambda-delta/common/output.ml b/helm/software/lambda-delta/common/output.ml
index c2e43d460..8270c5d97 100644
--- a/helm/software/lambda-delta/common/output.ml
+++ b/helm/software/lambda-delta/common/output.ml
@@ -11,8 +11,7 @@
 
 module P = Printf
 module L = Log
-
-let icm = ref 0
+module O = Options
 
 type reductions = {
    beta   : int;
@@ -70,6 +69,4 @@ let print_reductions () =
    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 "  Relocated nodes (icm):      %7u" !icm)
-
-let indexes = ref false
+   L.warn (P.sprintf "  Relocated nodes (icm):      %7u" !O.icm)