]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/basic_ag/bagOutput.ml
- improved logging
[helm.git] / helm / software / lambda-delta / basic_ag / bagOutput.ml
index 589ce60f0f89912bfdf2eba98c448c01345ebceb..4e7ab87a027234fd21ecf276c77257a45b7ddbda 100644 (file)
@@ -84,6 +84,7 @@ let print_counters f c =
       c.tabbrs
    in
    let items = c.eabsts + c.eabbrs in
+   let locations = B.locations () in
    L.warn (P.sprintf "  Kernel representation summary (basic_ag)");
    L.warn (P.sprintf "    Total entry items:        %6u" items);
    L.warn (P.sprintf "      Declaration items:      %6u" c.eabsts);
@@ -96,6 +97,7 @@ let print_counters f c =
    L.warn (P.sprintf "      Application items:      %6u" c.tappls);
    L.warn (P.sprintf "      Abstraction items:      %6u" c.tabsts);
    L.warn (P.sprintf "      Abbreviation items:     %6u" c.tabbrs);
+   L.warn (P.sprintf "    Total binder locations:   %6u" locations);   
    f ()
 
 let indexes = ref false