package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

The Rocq Prover -- Core Binaries and Tools

Install

md5=8d522602d23e7a665631826dab9aa92b

sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be

Sourcetype summary = Summary.Synterp.frozen

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.

val start_module : 
  export ->
  Names.module_ident ->
  Names.ModPath.t ->
  summary ->
  Nametab.object_prefix

val start_modtype : 
  Names.module_ident ->
  Names.ModPath.t ->
  summary ->
  Nametab.object_prefix

Sourceval end_module : unit -> Nametab.object_prefix * summary * classified_objects

Sourceval end_modtype : unit -> Nametab.object_prefix * summary * classified_objects

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

On This Page