X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fcomplete_rg%2FcrgOutput.ml;h=f068181a789e034488563d970cde256d181d0969;hb=88977b2d546e547e23b046792fe2ad8f6ff192a4;hp=7463c769a47cb47ca53fbcfb180a9787ee74b523;hpb=fec20705af4705f8eb9542aece87769b82a6a6b4;p=helm.git

diff --git a/helm/software/helena/src/complete_rg/crgOutput.ml b/helm/software/helena/src/complete_rg/crgOutput.ml
index 7463c769a..f068181a7 100644
--- a/helm/software/helena/src/complete_rg/crgOutput.ml
+++ b/helm/software/helena/src/complete_rg/crgOutput.ml
@@ -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}
@@ -92,15 +94,15 @@ and count_binder f c e y b = match b with
       D.push_bind (f c) E.empty_node y b e
 
 let count_entity f c = function
-   | _, _, u, E.Abst w -> 
+   | _, _, u, E.Abst (_, w) -> 
       let c = {c with
          eabsts = succ c.eabsts; nodes = succ c.nodes; uris = u :: c.uris
       } in
       count_term f c D.ESort w
-   | _, _, _, E.Abbr v ->  
+   | _, _, _, E.Abbr (_, v) ->  
       let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in
       count_term f c D.ESort v
-   | _, _, _, E.Void   -> assert false
+   | _, _, _, E.Void        -> assert false
 
 let print_counters f c =
    let terms =
@@ -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 =