Module `Coqdeplib.Loadpath`Source

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 =

| ExactMatches of filename list
| 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

Source

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

Source

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

Source

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

Source

val add_known : 
  State.t ->
  bool ->
  root ->
  dirname ->
  dirpath ->
  basename ->
  unit

Source

val 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

Source

val absolute_file_name : 
  filename_concat:(string -> string -> string) ->
  string ->
  string option ->
  string

Install

Dune Dependency

Authors

Maintainers

Sources

doc/rocq-runtime.coqdeplib/Coqdeplib/Loadpath/index.html

Module `Coqdeplib.Loadpath`Source

package rocq-runtime

Install

Dune Dependency

Authors

Maintainers

Sources

doc/rocq-runtime.coqdeplib/Coqdeplib/Loadpath/index.html

Module Coqdeplib.LoadpathSource

Module `Coqdeplib.Loadpath`Source