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 physical : t -> CUnix.physical_path

Get the physical path 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 with a physical path. Raises Not_found if there is none.

val find_with_logical_path : Names.DirPath.t -> t list

get the list of load paths that correspond to a given logical path

val find_extra_dep_with_logical_path : ?loc:Loc.t -> from:Names.DirPath.t -> file:string -> unit -> CUnix.physical_path

finds a file rooted in from.

  • raises UserError

    if the file is not found

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 locate_error =
| LibUnmappedDir
| LibNotFound

Locate a library in the load path

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

Locates a library by implicit name.

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 true for -R, false for -Q in command line

*)
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