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.library/Lib/Interp/index.html

Module Lib.InterpSource

Sourceval find_opening_node : ?loc:Loc.t -> Names.Id.t -> summary node

Returns the opening node of a given name

Sourceval add_entry : summary node -> unit
Sourceval add_leaf_entry : Libobject.t -> unit
Sourceval open_section : Names.Id.t -> unit

Sections

Sourceval close_section : unit -> discharged_item list

close_section needs to redo Export, so the complete implementation needs to involve Declaremods.

Modules and module types
Sourcetype frozen
Sourceval freeze : unit -> frozen
Sourceval unfreeze : frozen -> unit
Sourceval init : unit -> unit
Sourceval drop_objects : frozen -> frozen

Keep only the libobject structure, not the objects themselves

Sourceval declare_info : Library_info.t -> unit