Interp (coq-core.Lib.Interp)

type summary = Summary.Interp.frozen

type classified_objects = {

substobjs : Libobject.t list;

keepobjs : Libobject.t list;

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

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

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