]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/lambda-delta/common/library.ml
some interfaces improved
[helm.git] / helm / software / lambda-delta / common / library.ml
index 8dec0dd5d122614ca10ddfc61c04644b8fa9d61d..c60a227e76c65e425783f007dc7c4a003f641bfc 100644 (file)
@@ -42,15 +42,15 @@ let close_entry frm =
 
 (* interface functions ******************************************************)
 
-let export_item export_obj si g = function
-   | Some obj ->
-      let _, uri, bind = obj in
+let export_unit export_entry si g = function
+   | Some entry ->
+      let _, uri, bind = entry in
       let path = path_of_uri uri in
       let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in
       let och = open_out (path ^ obj_ext) in
       let frm = Format.formatter_of_out_channel och in
       Format.pp_set_margin frm max_int;
       Format.fprintf frm "@[<v>%t%t%t%a%t@]@." 
-         pp_head pp_doctype (open_entry si g) export_obj obj close_entry;  
+         pp_head pp_doctype (open_entry si g) export_entry entry close_entry;  
       close_out och
    | None     -> ()