update in helena

[helm.git] / helm / software / helena / src / complete_rg / crgOutput.ml

diff --git a/helm/software/helena/src/complete_rg/crgOutput.ml b/helm/software/helena/src/complete_rg/crgOutput.ml
index 7463c769a47cb47ca53fbcfb180a9787ee74b523..f068181a789e034488563d970cde256d181d0969 100644 (file)
--- 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 =