]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/basic_ag/bagOutput.ml
- new attributes system
[helm.git] / helm / software / helena / src / basic_ag / bagOutput.ml
index 4d0a1c07b1b2e834fed3861c84535459ab4a202e..0fbc039b20a228821108cc86d911c806fc1ca06a 100644 (file)
@@ -68,13 +68,13 @@ and count_term f c = function
       count_term f c t
 
 let count_entity f c = function
-   | _, _, E.Abst (_, w) -> 
+   | _, _, _, E.Abst w -> 
       let c = {c with eabsts = succ c.eabsts} in
       count_term f c w
-   | _, _, E.Abbr v      -> 
+   | _, _, _, E.Abbr v -> 
       let c = {c with eabbrs = succ c.eabbrs} in
       count_term f c v
-   | _, _, E.Void        -> assert false
+   | _, _, _, E.Void   -> assert false
 
 let print_counters f c =
    let terms =
@@ -82,7 +82,7 @@ let print_counters f c =
       c.tabbrs
    in
    let items = c.eabsts + c.eabbrs in
-   let locations = J.locations () in
+   let locations = J.marks () in
    L.warn level (P.sprintf "Kernel representation summary (basic_ag)");
    L.warn level (P.sprintf "  Total entry items:        %7u" items);
    L.warn level (P.sprintf "    Declaration items:      %7u" c.eabsts);
@@ -106,7 +106,7 @@ let name err och a =
    E.name err f a
 
 let res a l och =
-   let err () = P.fprintf och "#%u" l in
+   let err () = P.fprintf och "#%s" (J.to_string l) in
    if !G.indexes then err () else name err och a
 
 let rec pp_term c och = function
@@ -115,7 +115,7 @@ let rec pp_term c och = function
       let f s = P.fprintf och "%s" s in
       H.string_of_sort err f h 
    | Z.LRef i                 -> 
-      let err () = P.fprintf och "#%u" i in
+      let err () = P.fprintf och "#%s" (J.to_string i) in
       let f a _ = name err och a in
       if !G.indexes then err () else Z.get err f c i
    | Z.GRef s                    -> P.fprintf och "$%s" (U.string_of_uri s)