Module `Loadpath`

type t: Type of loadpath bindings.

val logical : t -> Names.DirPath.t: Get the logical path (Coq module hierarchy) of a loadpath.

val pp : t -> Pp.t: Print a load path

val get_load_paths : unit -> t list: Get the current loadpath association.

val remove_load_path : CUnix.physical_path -> unit: Remove the current logical path binding associated to a given physical path, if any.

val find_load_path : CUnix.physical_path -> t: Get the binding associated to a physical path. Raises Not_found if there is none.

val locate_file : string -> string: Locate a file among the registered paths. Do not use this function, as it does not respect the visibility of paths.

type library_location = | LibLoaded | LibInPath: Locate a library in the load path

type locate_error = | LibUnmappedDir | LibNotFound
type 'a locate_result = ('a, locate_error) Stdlib.result

val locate_qualified_library : ?⁠root:Names.DirPath.t -> ?⁠warn:bool -> Libnames.qualid -> (library_location * Names.DirPath.t * CUnix.physical_path) locate_result

val try_locate_absolute_library : Names.DirPath.t -> string

Extending the Load Path

type vo_path = { unix_path : string; Filesystem path containing vo/ml files coq_path : Names.DirPath.t; Coq prefix for the path implicit : bool; implicit = true avoids having to qualify with coq_path has_ml : bool; If has_ml is true, the directory will also be added to the ml include path recursive : bool; recursive will determine whether we explore sub-directories }: Adds a path to the Coq and ML paths

val add_vo_path : vo_path -> unit