package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

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

module Error : sig ... end
val locate_qualified_library : ?root:Names.DirPath.t -> Libnames.qualid -> (Names.DirPath.t * CUnix.physical_path, Error.t) Stdlib.Result.t
val locate_absolute_library : Names.DirPath.t -> (CUnix.physical_path, Error.t) Stdlib.Result.t

Locates a library by implicit name.

  • returns

    LibUnmappedDir if the library is not in the path

  • returns

    LibNotFound if there is no corresponding file in the path

Extending the Load Path
type 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 true for -R, false for -Q in command line

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

val add_vo_path : vo_path -> unit
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct