X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fautomath%2FautOutput.ml;h=2f1a4d91c4715ab67b739c40f6b5e1348a734c48;hb=b68e52f889215ce2c21c3d771f59b2d2057d53c1;hp=ffbdfdb2096eeac175e3e86ee1af854c60fe100a;hpb=960ed22a5a6c415e2cf0ec9e8f5680d75c3ca0cd;p=helm.git

diff --git a/helm/software/lambda-delta/automath/autOutput.ml b/helm/software/lambda-delta/automath/autOutput.ml
index ffbdfdb20..2f1a4d91c 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,14 @@ 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 iag =
+      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);
+      L.warn (P.sprintf "    Implicit after global:    %7u" iag);
+      f ()
+   in
+   R.get_counters f c