]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/common/output.ml
- we completed the text parser fixing the syntactic shortcuts
[helm.git] / helm / software / lambda-delta / common / output.ml
index c2e43d460a2e5dc1ecc278c9b325089dbd302810..8270c5d9721951b9f1295ad2949662f4adbce07e 100644 (file)
@@ -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)