- conditional compilation continues ...

[helm.git] / helm / software / helena / src / automath / autOutput.ml

diff --git a/helm/software/helena/src/automath/autOutput.ml b/helm/software/helena/src/automath/autOutput.ml
index a1f5ae18c56e8c1fa97a2885ad9dbc3e144ece78..f9272867c58158d385a94b68f74f9237e4d93d6c 100644 (file)
--- 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