X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fautomath%2FautOutput.ml;h=f9272867c58158d385a94b68f74f9237e4d93d6c;hb=600fba840c748f67593838673a6eb40eab9b68e5;hp=a1f5ae18c56e8c1fa97a2885ad9dbc3e144ece78;hpb=edf9e34100f49d4aa5ba8f3ce53e34af7718d88e;p=helm.git

diff --git a/helm/software/helena/src/automath/autOutput.ml b/helm/software/helena/src/automath/autOutput.ml
index a1f5ae18c..f9272867c 100644
--- a/helm/software/helena/src/automath/autOutput.ml
+++ b/helm/software/helena/src/automath/autOutput.ml
@@ -37,6 +37,8 @@ let initial_counters = {
    sorts = 0; grefs = 0; appls = 0; absts = 0; pars = 0; xnodes = 0
 }
 
+IFDEF SUMMARY THEN
+
 let rec count_term f c = function
    | A.Sort _         -> 
       f {c with sorts = succ c.sorts; xnodes = succ c.xnodes}
@@ -91,6 +93,8 @@ let print_counters f c =
    L.warn level (KP.sprintf "    + Abbreviation nodes:   %7u" c.xnodes);
    f ()
 
+IFDEF PREPROCESS THEN
+
 let print_process_counters f c =
    let f iao iar iac iag =
       L.warn level (KP.sprintf "Automath process summary");
@@ -101,3 +105,7 @@ let print_process_counters f c =
       f ()
    in
    AA.get_counters f c
+
+END
+
+END