CheckLibrary (rocq-runtime.Coq_checklib.CheckLibrary)

type section_path = {

dirpath : string list;

basename : string;

}

type object_file =

| PhysicalFile of CUnix.physical_path

| LogicalFile of section_path

type logical_path = Names.DirPath.t

val default_root_prefix : Names.DirPath.t

val add_load_path : (CUnix.physical_path * logical_path) -> unit

val recheck_library : Safe_typing.safe_environment -> norec:object_file list -> admit:object_file list -> check:object_file list -> Safe_typing.safe_environment * Names.Cset.t Names.Cmap.t