]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_rg/brgOutput.ml
update in helena
[helm.git] / helm / software / helena / src / basic_rg / brgOutput.ml
index 0c692045ed7db3e6c7f13a9ffc7e196ee65e18d0..7bb9ce4363a73c9d91cf64cf1719224b521077c8 100644 (file)
@@ -52,6 +52,8 @@ let initial_counters = {
    uris = []; nodes = 0; xnodes = 0
 }
 
+IFDEF SUMMARY THEN
+
 let rec count_term_binder f c e = function
    | B.Abst (_, _, w) ->
       let c = {c with tabsts = succ c.tabsts; nodes = succ c.nodes} in
@@ -94,15 +96,15 @@ and count_term f c e = function
       count_term_binder f c e b
 
 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 B.empty w
-   | _, _, _, E.Abbr v ->  
+   | _, _, _, E.Abbr (_, v) ->  
       let c = {c with eabbrs = succ c.eabbrs; xnodes = succ c.xnodes} in
       count_term f c B.empty 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
+
 (* lenv/term pretty printing ************************************************)
 
 let name err och a =
@@ -191,7 +195,11 @@ let specs = {
    L.pp_term = pp_term; L.pp_lenv = pp_lenv
 }
 
+IFDEF OBJECTS THEN
+
 (* term xml printing ********************************************************)
 
 let export_term st =
    BD.crg_of_brg (XD.export_term st)  
+
+END