package rocq-runtime

  1. Overview
  2. Docs
package rocq-runtime
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Coqdeplib.LoadpathSource

Sourceval get_extension : string -> string list -> string * string

To move

Sourcetype basename = string
Sourcetype dirname = string
Sourcetype dir = string option
Sourcetype filename = string
Sourcetype dirpath = string list
Sourcetype root = filename * dirpath
Sourcetype result =
  1. | ExactMatches of filename list
  2. | PartialMatchesInSameRoot of root * filename list
Sourcemodule State : sig ... end
Sourceval get_worker_path : State.t -> string
Sourceval search_v_known : State.t -> ?from:dirpath -> dirpath -> result option
Sourceval search_other_known : State.t -> ?from:dirpath -> dirpath -> result option
Sourceval is_in_coqlib : State.t -> ?from:dirpath -> dirpath -> bool
Sourceval add_current_dir : State.t -> System.unix_path -> unit
Sourceval add_q_include : State.t -> System.unix_path -> string -> unit
Sourceval add_r_include : State.t -> System.unix_path -> string -> unit
Sourceval add_norec_dir_import : (bool -> root -> dirname -> dirpath -> basename -> unit) -> dirname -> dirpath -> unit

Simply add this directory and imports it, no subdirs. This is used by the implicit adding of the current path.

Sourceval add_rec_dir_no_import : (bool -> root -> dirname -> dirpath -> basename -> unit) -> dirname -> dirpath -> unit

-Q semantic: go in subdirs but only full logical paths are known.

Sourceval add_rec_dir_import : (bool -> root -> dirname -> dirpath -> basename -> unit) -> dirname -> dirpath -> unit

-R semantic: go in subdirs and suffixes of logical paths are known.

Sourceval add_known : State.t -> bool -> root -> dirname -> dirpath -> basename -> unit
Sourceval add_coqlib_known : State.t -> bool -> root -> dirname -> dirpath -> basename -> unit
Sourceval find_dir_logpath : string -> string list

find_dir_logpath phys_dir Return the logical path of directory dir if it has been given one. Raise Not_found otherwise. In particular we can check if "." has been attributed a logical path after processing all options and silently give the default one if it hasn't. We may also use this to warn if ap hysical path is met twice.

Sourceval absolute_dir : string -> string
Sourceval absolute_file_name : filename_concat:(string -> string -> string) -> string -> string option -> string
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