Module 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 * Mod_checking.opaques