X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fautomath%2FautOutput.ml;h=6ca42e6c640a165a65e2955a2421b7d6d7b07c8a;hb=2b821e608cc1fceebc13e85867a244fe02edf71e;hp=ffbdfdb2096eeac175e3e86ee1af854c60fe100a;hpb=016f069da6221053873b4d505716ef1bd80f08b6;p=helm.git

diff --git a/helm/software/lambda-delta/automath/autOutput.ml b/helm/software/lambda-delta/automath/autOutput.ml
index ffbdfdb20..6ca42e6c6 100644
--- a/helm/software/lambda-delta/automath/autOutput.ml
+++ b/helm/software/lambda-delta/automath/autOutput.ml
@@ -12,6 +12,7 @@
 module P = Printf
 module L = Log
 module A = Aut
+module R = AutProcess
 
 type counters = {
    sections: int;
@@ -85,3 +86,13 @@ let print_counters f c =
    L.warn (P.sprintf "    Global Int. Complexity:   unknown");
    L.warn (P.sprintf "      + Abbreviation nodes:   %7u" c.xnodes);
    f ()
+
+let print_process_counters f c =
+   let f iao iar iac =
+      L.warn (P.sprintf "  Automath process summary");
+      L.warn (P.sprintf "    Implicit after opening:   %7u" iao);
+      L.warn (P.sprintf "    Implicit after reopening: %7u" iar);
+      L.warn (P.sprintf "    Implicit after closing:   %7u" iac);
+      f ()
+   in
+   R.get_counters f c