package coq

  1. Overview
  2. Docs
Formal proof management system

Install 

dune-project
 Dependency

coq.inria.fr Edit opam file Versions (40)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors.

Maintainers

  1. C
    coqdev@inria.fr

Sources

coq-8.14.1.tar.gz
sha256=3cbfc1e1a72b16d4744f5b64ede59586071e31d9c11c811a0372060727bfd9c3

doc/coq-core.vernac/Loadpath/index.html

Module LoadpathSource

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

Sourcetype t

Type of loadpath bindings.

Sourceval logical : t -> Names.DirPath.t

Get the logical path (Coq module hierarchy) of a loadpath.

Sourceval pp : t -> Pp.t

Print a load path

Sourceval get_load_paths : unit -> t list

Get the current loadpath association.

Sourceval remove_load_path : CUnix.physical_path -> unit

Remove the current logical path binding associated to a given physical path, if any.

Sourceval find_load_path : CUnix.physical_path -> t

Get the binding associated to a physical path. Raises Not_found if there is none.

Sourceval 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.

Sourcetype library_location =
  1. | LibLoaded
  2. | LibInPath

Locate a library in the load path

Sourcetype locate_error =
  1. | LibUnmappedDir
  2. | LibNotFound
Sourcetype 'a locate_result = ('a, locate_error) result
Sourceval locate_qualified_library : ?root:Names.DirPath.t -> ?warn:bool -> Libnames.qualid -> (library_location * Names.DirPath.t * CUnix.physical_path) locate_result

Locates a library by implicit name.

  • raises LibNotFound

    if there is no corresponding file in the path

Sourceval try_locate_absolute_library : Names.DirPath.t -> string
Extending the Load Path
Sourcetype vo_path = {
  1. unix_path : string;
    (*

    Filesystem path containing vo/ml files

    *)
  2. coq_path : Names.DirPath.t;
    (*

    Coq prefix for the path

    *)
  3. implicit : bool;
    (*

    implicit = true avoids having to qualify with coq_path

    *)
  4. has_ml : bool;
    (*

    If has_ml is true, the directory will also be added to the ml include path

    *)
  5. recursive : bool;
    (*

    recursive will determine whether we explore sub-directories

    *)
}

Adds a path to the Coq and ML paths

Sourceval add_vo_path : vo_path -> unit