Module `Lib`

type is_type = bool
type export_flag = | Export | Import
type export = (export_flag * Libobject.open_filter) option

val make_oname : Nametab.object_prefix -> Names.Id.t -> Libobject.object_name
val make_foname : Names.Id.t -> Libobject.object_name
val oname_prefix : Libobject.object_name -> Nametab.object_prefix

type node = | CompilingLibrary of Nametab.object_prefix | OpenedModule of is_type * export * Nametab.object_prefix * Summary.frozen | OpenedSection of Nametab.object_prefix * Summary.frozen

val node_prefix : node -> Nametab.object_prefix: Extract the object_prefix component. Note that it is the prefix of the objects *inside* this node, eg in Module M. we have OpenedModule with prefix containing M.

type library_segment = (node * Libobject.t list) list
type classified_objects = { substobjs : Libobject.t list; keepobjs : Libobject.t list; anticipateobjs : Libobject.t list; }

...

val add_entry : node -> unit
val add_leaf_entry : Libobject.t -> unit

...

val add_leaf : Libobject.obj -> unit

...

val contents : unit -> library_segment

Functions relative to current path

val prefix : unit -> Nametab.object_prefix: User-side names

val cwd : unit -> Names.DirPath.t
val cwd_except_section : unit -> Names.DirPath.t
val current_dirpath : bool -> Names.DirPath.t
val make_path : Names.Id.t -> Libnames.full_path
val make_path_except_section : Names.Id.t -> Libnames.full_path
val current_mp : unit -> Names.ModPath.t: Kernel-side names

val make_kn : Names.Id.t -> Names.KerName.t
val sections_are_opened : unit -> bool: Are we inside an opened section

val sections_depth : unit -> int
val is_module_or_modtype : unit -> bool: Are we inside an opened module type

val is_modtype : unit -> bool
val is_modtype_strict : unit -> bool
val is_module : unit -> bool
val find_opening_node : Names.Id.t -> node: Returns the opening node of a given name

Modules and module types

val start_module : export -> Names.module_ident -> Names.ModPath.t -> Summary.frozen -> Nametab.object_prefix
val start_modtype : Names.module_ident -> Names.ModPath.t -> Summary.frozen -> Nametab.object_prefix
val end_module : unit -> Nametab.object_prefix * Summary.frozen * classified_objects
val end_modtype : unit -> Nametab.object_prefix * Summary.frozen * classified_objects

Compilation units

val start_compilation : Names.DirPath.t -> Names.ModPath.t -> unit
val end_compilation : Names.DirPath.t -> Nametab.object_prefix * classified_objects
val library_dp : unit -> Names.DirPath.t: The function library_dp returns the DirPath.t of the current compiling library (or default_library)

val dp_of_mp : Names.ModPath.t -> Names.DirPath.t: Extract the library part of a name even if in a section

val split_modpath : Names.ModPath.t -> Names.DirPath.t * Names.Id.t list
val library_part : Names.GlobRef.t -> Names.DirPath.t

Sections

val open_section : Names.Id.t -> unit
val close_section : unit -> unit

We can get and set the state of the operations (used in `States`).

type frozen

val freeze : unit -> frozen
val unfreeze : frozen -> unit
val drop_objects : frozen -> frozen: Keep only the libobject structure, not the objects themselves

val init : unit -> unit
val section_segment_of_constant : Names.Constant.t -> Cooking.cooking_info: Section management for discharge

val section_segment_of_inductive : Names.MutInd.t -> Cooking.cooking_info
val section_segment_of_reference : Names.GlobRef.t -> Cooking.cooking_info
val section_instance : Names.GlobRef.t -> Constr.t array
val is_in_section : Names.GlobRef.t -> bool

Discharge: decrease the section level if in the current section

val discharge_proj_repr : Names.Projection.Repr.t -> Names.Projection.Repr.t