Added ntry and nassumption tactics

[helm.git] / helm / software / lambda-delta / toplevel / metaOutput.ml

diff --git a/helm/software/lambda-delta/toplevel/metaOutput.ml b/helm/software/lambda-delta/toplevel/metaOutput.ml
index 2d5bc3ad5c946ac3bbab196e9e0c6d92ac3d42cf..5fe20f0f428ed0179ec0b1ed7a7975b676df7f1c 100644 (file)
--- a/helm/software/lambda-delta/toplevel/metaOutput.ml
+++ b/helm/software/lambda-delta/toplevel/metaOutput.ml
@@ -74,18 +74,18 @@ let print_counters f c =
    let pars = c.pabsts + c.pappls in
    let items = c.eabsts + c.eabbrs in
    L.warn (P.sprintf "  Intermediate representation summary");
-   L.warn (P.sprintf "    Total entry items:        %6u" items);
-   L.warn (P.sprintf "      Declaration items:      %6u" c.eabsts);
-   L.warn (P.sprintf "      Definition items:       %6u" c.eabbrs);
-   L.warn (P.sprintf "    Total parameter items:    %6u" pars);
-   L.warn (P.sprintf "      Application items:      %6u" c.pappls);
-   L.warn (P.sprintf "      Abstraction items:      %6u" c.pabsts);
-   L.warn (P.sprintf "    Total term items:         %6u" terms);
-   L.warn (P.sprintf "      Sort items:             %6u" c.tsorts);
-   L.warn (P.sprintf "      Local reference items:  %6u" c.tlrefs);
-   L.warn (P.sprintf "      Global reference items: %6u" c.tgrefs);
-   L.warn (P.sprintf "      Application items:      %6u" c.tappls);
-   L.warn (P.sprintf "      Abstraction items:      %6u" c.tabsts);
+   L.warn (P.sprintf "    Total entry items:        %7u" items);
+   L.warn (P.sprintf "      Declaration items:      %7u" c.eabsts);
+   L.warn (P.sprintf "      Definition items:       %7u" c.eabbrs);
+   L.warn (P.sprintf "    Total parameter items:    %7u" pars);
+   L.warn (P.sprintf "      Application items:      %7u" c.pappls);
+   L.warn (P.sprintf "      Abstraction items:      %7u" c.pabsts);
+   L.warn (P.sprintf "    Total term items:         %7u" terms);
+   L.warn (P.sprintf "      Sort items:             %7u" c.tsorts);
+   L.warn (P.sprintf "      Local reference items:  %7u" c.tlrefs);
+   L.warn (P.sprintf "      Global reference items: %7u" c.tgrefs);
+   L.warn (P.sprintf "      Application items:      %7u" c.tappls);
+   L.warn (P.sprintf "      Abstraction items:      %7u" c.tabsts);
    f ()
 
 let string_of_sort = function
@@ -104,6 +104,9 @@ let pp_list pp opend sep closed frm l =
    in
    if l = [] then () else F.fprintf frm "%s%a%s" opend aux l closed
 
+let pp_rev_list pp opend sep closed frm l =
+   pp_list pp opend sep closed frm (List.rev l)
+
 let rec pp_args frm args = pp_list pp_term "(" "," ")" frm args
 
 and pp_term frm = function
@@ -121,7 +124,7 @@ and pp_term frm = function
 let pp_par frm (id, w) =
     F.fprintf frm "%s:%a" id pp_term w
 
-let pp_pars = pp_list pp_par "[" "," "]"
+let pp_pars = pp_rev_list pp_par "[" "," "]"
 
 let pp_body frm = function
    | None            -> ()