Skip to content

Commit

Permalink
[library] Remove unused API and exported types.
Browse files Browse the repository at this point in the history
This is not needed anymore since coq#18424 I believe.
  • Loading branch information
ejgallego committed Jun 8, 2024
1 parent 6a2dd90 commit c7a5d5d
Show file tree
Hide file tree
Showing 2 changed files with 0 additions and 10 deletions.
2 changes: 0 additions & 2 deletions vernac/library.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
8 changes: 0 additions & 8 deletions vernac/library.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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 *)
Expand Down

0 comments on commit c7a5d5d

Please sign in to comment.