]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/complete_rg/crgOutput.ml
- conditional compilation continues ...
[helm.git] / helm / software / helena / src / complete_rg / crgOutput.ml
index 7463c769a47cb47ca53fbcfb180a9787ee74b523..535ec2bebccd5e8dc8f8ffd81d6c1f4e118c16c0 100644 (file)
@@ -47,6 +47,8 @@ let initial_counters = {
    uris = []; nodes = 0; xnodes = 0
 }
 
+IFDEF SUMMARY THEN
+
 let rec count_term f c e = function
    | D.TSort _         -> 
       f {c with tsorts = succ c.tsorts; nodes = succ c.nodes}
@@ -127,6 +129,8 @@ let print_counters f c =
    L.warn level (KP.sprintf "    + Abbreviation nodes:   %7u" nodes);
    f ()
 
+END
+
 (* term/environment pretty printer ******************************************)
 
 let pp_b_attrs out a =