package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t
val logical : t -> Names.DirPath.t
val pp : t -> Pp.t
val get_load_paths : unit -> t list
val remove_load_path : CUnix.physical_path -> unit
val find_load_path : CUnix.physical_path -> t
val locate_file : string -> string
type library_location =
  1. | LibLoaded
  2. | LibInPath
type locate_error =
  1. | LibUnmappedDir
  2. | LibNotFound
type !'a locate_result = ('a, locate_error) 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
type vo_path = {
  1. unix_path : string;
  2. coq_path : Names.DirPath.t;
  3. implicit : bool;
  4. has_ml : bool;
  5. recursive : bool;
}
val add_vo_path : vo_path -> unit