Module Loadpath

* Load paths.

A load path is a physical path in the file system; to each load path is associated a Coq DirPath.t (the "logical" path of the physical path).

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 add_ml =
| AddNoML
| AddTopML
| AddRecML

Adds a path to the Coq and ML paths

type vo_path_spec = {
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 : add_ml;

If has_ml is true, the directory will also be search for plugins

}
type coq_path_spec =
| VoPath of vo_path_spec
| MlPath of string
type coq_path = {
path_spec : coq_path_spec;
recursive : bool;
}
val add_coq_path : coq_path -> unit