X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fbasic_ag%2FbagOutput.ml;h=a97219120dc2cbc1098bafb22ffd24b874efe55a;hb=f00757144b2cd7e6457fed55dbc1309d11a542dc;hp=d6633bcd863b5a3615972af0f8175c9459472118;hpb=8a4c83c6341976f2bb70eb44a0c70f2aa95ad3ea;p=helm.git diff --git a/helm/software/lambda-delta/basic_ag/bagOutput.ml b/helm/software/lambda-delta/basic_ag/bagOutput.ml index d6633bcd8..a97219120 100644 --- a/helm/software/lambda-delta/basic_ag/bagOutput.ml +++ b/helm/software/lambda-delta/basic_ag/bagOutput.ml @@ -13,6 +13,7 @@ module P = Printf module F = Format module U = NUri module L = Log +module Y = Entity module H = Hierarchy module O = Output module B = Bag @@ -62,21 +63,13 @@ and count_term f c = function let f c = count_term_binder f c b in count_term f c t -let count_obj_binder f c = function - | B.Abst w -> +let count_entity f c = function + | _, _, Y.Abst w -> let c = {c with eabsts = succ c.eabsts} in count_term f c w - | B.Abbr v -> + | _, _, Y.Abbr v -> let c = {c with eabbrs = succ c.eabbrs} in count_term f c v - | B.Void -> f c - -let count_obj f c (_, _, b) = - count_obj_binder f c b - -let count_item f c = function - | Some obj -> count_obj f c obj - | None -> f c let print_counters f c = let terms =