X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fautomath%2FautOutput.ml;h=5b415ff0bee1be9416d4568fa9c91842843c3a68;hb=3a4c39fc9c938ca155f0e807525cd38eec240a0d;hp=f9467d63e1d10468505e5bb40a95a7fd8bee02ba;hpb=79684e8bd0f54b5c88fff981366bd8c78dd0fbe9;p=helm.git diff --git a/helm/software/lambda-delta/automath/autOutput.ml b/helm/software/lambda-delta/automath/autOutput.ml index f9467d63e..5b415ff0b 100644 --- a/helm/software/lambda-delta/automath/autOutput.ml +++ b/helm/software/lambda-delta/automath/autOutput.ml @@ -50,7 +50,7 @@ let rec count_term f c = function let f c = count_term f c t in count_term f c w -let count_unit f c = function +let count_entity f c = function | A.Section _ -> f {c with sections = succ c.sections} | A.Context _ -> @@ -68,14 +68,14 @@ let count_unit f c = function let print_counters f c = let terms = c.sorts + c.grefs + c.appls + c.absts in - let units = c.sections + c.contexts + c.blocks + c.decls + c.defs in + let entities = c.sections + c.contexts + c.blocks + c.decls + c.defs in L.warn (P.sprintf " Automath representation summary"); - L.warn (P.sprintf " Total book units: %7u" units); - L.warn (P.sprintf " Section units: %7u" c.sections); - L.warn (P.sprintf " Context units: %7u" c.contexts); - L.warn (P.sprintf " Block units: %7u" c.blocks); - L.warn (P.sprintf " Declaration units: %7u" c.decls); - L.warn (P.sprintf " Definition units: %7u" c.defs); + L.warn (P.sprintf " Total book entities: %7u" entities); + L.warn (P.sprintf " Section entities: %7u" c.sections); + L.warn (P.sprintf " Context entities: %7u" c.contexts); + L.warn (P.sprintf " Block entities: %7u" c.blocks); + L.warn (P.sprintf " Declaration entities: %7u" c.decls); + L.warn (P.sprintf " Definition entities: %7u" c.defs); L.warn (P.sprintf " Total Parameter items: %7u" c.pars); L.warn (P.sprintf " Application items: %7u" c.pars); L.warn (P.sprintf " Total term items: %7u" terms);