Module Coq_checklib.CheckLibrary

type section_path = {
  1. dirpath : string list;
  2. basename : string;
}
type object_file =
  1. | PhysicalFile of CUnix.physical_path
  2. | 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