X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fbasic_ag%2FbagOutput.ml;h=689423167690dba237ec4d46e605e1bdc94aaae4;hb=88977b2d546e547e23b046792fe2ad8f6ff192a4;hp=41914b062caf82673450dc20705f16ce70356cca;hpb=fec20705af4705f8eb9542aece87769b82a6a6b4;p=helm.git

diff --git a/helm/software/helena/src/basic_ag/bagOutput.ml b/helm/software/helena/src/basic_ag/bagOutput.ml
index 41914b062..689423167 100644
--- a/helm/software/helena/src/basic_ag/bagOutput.ml
+++ b/helm/software/helena/src/basic_ag/bagOutput.ml
@@ -40,6 +40,8 @@ let initial_counters = {
    tcasts = 0; tappls = 0; tabsts = 0; tabbrs = 0
 }
 
+IFDEF SUMMARY THEN
+
 let rec count_term_binder f c = function
    | Z.Abst w ->
       let c = {c with tabsts = succ c.tabsts} in
@@ -69,13 +71,13 @@ and count_term f c = function
       count_term f c t
 
 let count_entity f c = function
-   | _, _, _, E.Abst w -> 
+   | _, _, _, E.Abst (_, w) -> 
       let c = {c with eabsts = succ c.eabsts} in
       count_term f c w
-   | _, _, _, E.Abbr v -> 
+   | _, _, _, E.Abbr (_, v) -> 
       let c = {c with eabbrs = succ c.eabbrs} in
       count_term f c v
-   | _, _, _, E.Void   -> assert false
+   | _, _, _, E.Void        -> assert false
 
 let print_counters f c =
    let terms =
@@ -99,6 +101,8 @@ let print_counters f c =
    L.warn level (KP.sprintf "  Total binder locations:   %7u" locations);   
    f ()
 
+END
+
 let name err och a =
    let f n = function 
       | true  -> KP.fprintf och "%s" n
@@ -155,7 +159,11 @@ let specs = {
    L.pp_term = pp_term; L.pp_lenv = pp_lenv
 }
 
+IFDEF OBJECTS THEN
+
 (* term xml printing ********************************************************)
 
 let export_term st =
    ZD.crg_of_bag (XD.export_term st)  
+
+END