package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

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

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.1.0.tar.gz
sha256=b236dc44f92e1eeca6877c7ee188a90c2303497fe7beb99df711ed5a7ce0d824

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

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