From c7a5d5d978461d7287ac5ed947bf6bcd3a89b513 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 8 Jun 2024 15:43:48 +0200 Subject: [PATCH] [library] Remove unused API and exported types. This is not needed anymore since #18424 I believe. --- vernac/library.ml | 2 -- vernac/library.mli | 8 -------- 2 files changed, 10 deletions(-) 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 *)