]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/toplevel/top.ml
- helena: the improved attribute system allows to export the sorts of Pi's
[helm.git] / helm / software / helena / src / toplevel / top.ml
index 2db38afb88f75591d42e9654857156c3ae915762..535450c1f155d7b6a2a556818833eaa6e77c0d10 100644 (file)
@@ -97,9 +97,7 @@ let xlate_entity st entity = match !G.kernel, entity with
 let pp_progress e =
    let f _ na u =
       let s = U.string_of_uri u in
-      let err () = L.warn 2 (P.sprintf "<%s>" s) in
-      let f i = L.warn 2 (P.sprintf "[%u] <%s>" i s) in
-      E.apix err f na
+      L.warn 2 (P.sprintf "[%u] <%s>" na.E.n_apix s)
    in
    match e with
       | CrgEntity e -> E.common f e