package coq-core

You can search for identifiers within the package.

in-package search v0.2.0

The Coq Proof Assistant -- Core Binaries and Tools

Install

Dune Dependency

coq.inria.fr Readme Edit opam file Versions (9)

Authors

T

The Coq development team, INRIA, CNRS, and contributors

Maintainers

T

The Coq development team <coqdev@inria.fr>

Sources

coq-8.19.0.tar.gz

md5=64b49dbc3205477bd7517642c0b9cbb6

sha512=02fb5b4fb575af79e092492cbec6dc0d15a1d74a07f827f657a72d4e6066532630e5a6d15be4acdb73314bd40b9a321f9ea0584e0ccfe51fd3a56353bd30db9b

doc/coq-core.library/Lib/Interp/index.html

Module `Lib.Interp`Source

Sourcetype summary = Summary.Interp.frozen

Sourcetype classified_objects = {

substobjs : Libobject.t list;
keepobjs : Libobject.t list;
anticipateobjs : Libobject.t list;

}

Sourceval classify_segment : Libobject.t list -> classified_objects

Sourceval find_opening_node : 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 -> unit

Modules and module types

Source

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

Source

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 list -> unit

On This Page

Modules and module types