X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fcommon%2Foutput.ml;fp=helm%2Fsoftware%2Flambda-delta%2Fsrc%2Fcommon%2Foutput.ml;h=1124764885c871d364e7cfd3d6d3c048a17a77ec;hb=651d745df2454a9e232aff3c9d8bf3e77653936d;hp=38ebf8a34842c55d9da446989e4276d4925380fa;hpb=fb6fee82bb9172e15b1a7bc7e20641627f593fcc;p=helm.git

diff --git a/helm/software/lambda-delta/src/common/output.ml b/helm/software/lambda-delta/src/common/output.ml
index 38ebf8a34..112476488 100644
--- a/helm/software/lambda-delta/src/common/output.ml
+++ b/helm/software/lambda-delta/src/common/output.ml
@@ -16,7 +16,7 @@ module G = Options
 type reductions = {
    beta   : int;
    zeta   : int;
-   upsilon: int;
+   theta: int;
    tau    : int;
    ldelta : int;
    gdelta : int;
@@ -26,7 +26,7 @@ type reductions = {
 }
 
 let initial_reductions = {
-   beta = 0; upsilon = 0; tau = 0; zeta = 0; ldelta = 0; gdelta = 0;
+   beta = 0; theta = 0; tau = 0; zeta = 0; ldelta = 0; gdelta = 0;
    si = 0; lrt = 0; grt = 0
 }
 
@@ -35,12 +35,12 @@ let reductions = ref initial_reductions
 let clear_reductions () = reductions := initial_reductions
 
 let add 
-   ?(beta=0) ?(upsilon=0) ?(tau=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0) 
+   ?(beta=0) ?(theta=0) ?(tau=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0) 
    ?(si=0) ?(lrt=0) ?(grt=0) ()
 = reductions := {
    beta = !reductions.beta + beta;
    zeta = !reductions.zeta + zeta;
-   upsilon = !reductions.upsilon + upsilon;
+   theta = !reductions.theta + theta;
    tau = !reductions.tau + tau;
    ldelta = !reductions.ldelta + ldelta;
    gdelta = !reductions.gdelta + gdelta;
@@ -51,7 +51,7 @@ let add
 
 let print_reductions () =
    let r = !reductions in
-   let rs = r.beta + r.ldelta + r.zeta + r.upsilon + r.tau + r.gdelta in
+   let rs = r.beta + r.ldelta + r.zeta + r.theta + r.tau + r.gdelta in
    let prs = r.si + r.lrt + r.grt in
    let delta = r.ldelta + r.gdelta in
    let rt = r.lrt + r.grt in   
@@ -61,9 +61,9 @@ let print_reductions () =
    L.warn (P.sprintf "      Delta:                  %7u" delta);
    L.warn (P.sprintf "        Local:                %7u" r.ldelta);
    L.warn (P.sprintf "        Global:               %7u" r.gdelta);
-   L.warn (P.sprintf "      Zeta:                   %7u" r.zeta);
-   L.warn (P.sprintf "      Upsilon:                %7u" r.upsilon);
-   L.warn (P.sprintf "      Tau:                    %7u" r.tau);
+   L.warn (P.sprintf "      Theta:                  %7u" r.theta);
+   L.warn (P.sprintf "      Zeta for abbreviation:  %7u" r.zeta);
+   L.warn (P.sprintf "      Zeta for cast:          %7u" r.tau);
    L.warn (P.sprintf "    Pseudo reductions:        %7u" prs);
    L.warn (P.sprintf "      Reference typing:       %7u" rt);
    L.warn (P.sprintf "        Local:                %7u" r.lrt);