package coq-core

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type summary = Summary.Synterp.frozen
type classified_objects = {
  1. substobjs : Libobject.t list;
  2. keepobjs : Libobject.t list;
  3. anticipateobjs : Libobject.t list;
}
val classify_segment : Libobject.t list -> classified_objects
val find_opening_node : Names.Id.t -> summary node

Returns the opening node of a given name

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

Sections

val close_section : unit -> unit
Modules and module types
val end_module : unit -> Nametab.object_prefix * summary * classified_objects
val end_modtype : unit -> Nametab.object_prefix * summary * classified_objects
type frozen
val freeze : unit -> frozen
val unfreeze : frozen -> unit
val init : unit -> unit
val drop_objects : frozen -> frozen

Keep only the libobject structure, not the objects themselves

OCaml

Innovation. Community. Security.