diff --git a/vernac/library.ml b/vernac/library.ml
index 80535d941923..fe314527e31e 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -535,8 +535,6 @@ let save_library_to todo_proofs ~output_native_objects dir f =
     let fn = Filename.dirname f ^"/"^ Nativecode.mod_uid_of_dirpath dir in
     Nativelib.compile_library ast fn
 
-let save_library_raw f sum lib proofs = save_library_base f sum lib proofs
-
 let get_used_load_paths () =
   String.Set.elements
     (List.fold_left (fun acc (root, m) -> String.Set.add
diff --git a/vernac/library.mli b/vernac/library.mli
index 93fb4b56bd8d..f1b902d565fe 100644
--- a/vernac/library.mli
+++ b/vernac/library.mli
@@ -45,12 +45,6 @@ val require_library_syntax_from_dirpath
 
 (** {6 Start the compilation of a library } *)
 
-(** Segments of a library *)
-type seg_sum
-type seg_lib
-type seg_proofs = Opaques.opaque_disk
-type seg_vm = Vmlibrary.compiled_library
-
 (** End the compilation of a library and save it to a ".vo" file, or a
     ".vos" file, depending on the todo_proofs argument.
 
@@ -70,8 +64,6 @@ val save_library_to :
     [require_library_syntax_from_dirpath] *)
 val save_library : DirPath.t -> library_t
 
-val save_library_raw : string -> seg_sum -> seg_lib -> seg_proofs -> seg_vm -> unit
-
 (** {6 Interrogate the status of libraries } *)
 
   (** - Tell if a library is loaded *)