]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/toplevel/top.ml
- new attributes system
[helm.git] / helm / software / helena / src / toplevel / top.ml
index afa62555dfb68bcc04d6df64172c0d5f511963d1..d64857d324cc878c4b216522e8ccbbf0ff7861f6 100644 (file)
@@ -91,11 +91,11 @@ let xlate_entity entity = match !G.kernel, entity with
    | _, entity          -> entity
 
 let pp_progress e =
-   let f a u =
+   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 a
+      E.apix err f na
    in
    match e with
       | CrgEntity e -> E.common f e
@@ -267,7 +267,7 @@ let process st name =
    let lexbuf = Lexing.from_channel ich in 
    let st = process st lexbuf input in
    close_in ich; 
-   if !G.cc then XL.export_csys st.kst.S.cc; 
+(*   if !G.cc then XL.export_csys st.kst.S.cc; *)
    st, input
 
 let main =