package rocq-runtime

  1. Overview
  2. Docs

Module Rocq_packageSource

Sourcetype t = {
  1. name : string;
    (*

    Package name (fully-qualified findlib package name).

    *)
  2. dir : string;
    (*

    Directory holding the package's Rocq files (first argument of "-Q").

    *)
  3. logpath : string;
    (*

    Logical path associated to the directory (second argument of "-Q").

    *)
}

Rocq package (encoded as a findlib package).

Sourceval resolve : string list -> t list

resolve ps uses findlib to resolve the Rocq packages ps, together with their transitive dependencies. A user error is triggered if a package does not exist, or if a dependency loop is found.