Lib (u.75d6a066538fb738038ab1b402df0edb.coq.8.14.1.doc.coq-core.library.Lib)

This module provides a general mechanism to keep a trace of all operations and to backtrack (undo) those operations. It provides also the section mechanism (at a low level; discharge is not known at this step).

Sourcetype is_type = bool

Sourcetype export = bool option

Sourceval make_oname : Nametab.object_prefix -> Names.Id.t -> Libobject.object_name

Sourceval make_foname : Names.Id.t -> Libnames.full_path * Names.KerName.t

Sourcetype node =

| Leaf of Libobject.t
| CompilingLibrary of Nametab.object_prefix
| OpenedModule of is_type * export * Nametab.object_prefix * Summary.frozen
| OpenedSection of Nametab.object_prefix * Summary.frozen

Sourcetype library_segment = (Libobject.object_name * node) list

Sourcetype lib_atomic_objects = (Names.Id.t * Libobject.obj) list

Sourcetype lib_objects = (Names.Id.t * Libobject.t) list

Object iteration functions.

Source

val open_atomic_objects : 
  Libobject.open_filter ->
  int ->
  Nametab.object_prefix ->
  lib_atomic_objects ->
  unit

Source

val load_atomic_objects : 
  int ->
  Nametab.object_prefix ->
  lib_atomic_objects ->
  unit

Source

val subst_atomic_objects : 
  Mod_subst.substitution ->
  lib_atomic_objects ->
  lib_atomic_objects

Source

val classify_segment : 
  library_segment ->
  lib_objects * lib_objects * Libobject.t list

classify_segment seg verifies that there are no OpenedThings, clears ClosedSections and FrozenStates and divides Leafs according to their answers to the classify_object function in three groups: Substitute, Keep, Anticipate respectively. The order of each returned list is the same as in the input list.

Source

val segment_of_objects : 
  Nametab.object_prefix ->
  lib_objects ->
  library_segment

segment_of_objects prefix objs forms a list of Leafs

...

Low-level adding operations

Sourceval add_entry : Libobject.object_name -> node -> unit

Sourceval add_anonymous_entry : node -> unit

...

Adding operations (which call the cache method, and getting the current list of operations (most recent ones coming first).

Sourceval add_leaf : Names.Id.t -> Libobject.obj -> Libobject.object_name

Sourceval add_anonymous_leaf : ?cache_first:bool -> Libobject.obj -> unit

...

The function contents gives access to the current entire segment

Sourceval contents : unit -> library_segment

The function contents_after returns the current library segment, starting from a given section path.

Sourceval contents_after : Libobject.object_name -> library_segment

Functions relative to current path

Sourceval cwd : unit -> Names.DirPath.t

User-side names

Sourceval cwd_except_section : unit -> Names.DirPath.t

Sourceval current_dirpath : bool -> Names.DirPath.t

Sourceval make_path : Names.Id.t -> Libnames.full_path

Sourceval make_path_except_section : Names.Id.t -> Libnames.full_path

Sourceval current_mp : unit -> Names.ModPath.t

Kernel-side names

Sourceval make_kn : Names.Id.t -> Names.KerName.t

Sourceval sections_are_opened : unit -> bool

Are we inside an opened section

deprecated Use Global.sections_are_opened

Sourceval sections_depth : unit -> int

Sourceval is_module_or_modtype : unit -> bool

Are we inside an opened module type

Sourceval is_modtype : unit -> bool

Sourceval is_modtype_strict : unit -> bool

Sourceval is_module : unit -> bool

Sourceval current_mod_id : unit -> Names.module_ident

Sourceval find_opening_node : Names.Id.t -> node

Returns the opening node of a given name

Modules and module types

Source

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

Source

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

Source

val end_module : 
  unit ->
  Libobject.object_name
  * Nametab.object_prefix
  * Summary.frozen
  * library_segment

Source

val end_modtype : 
  unit ->
  Libobject.object_name
  * Nametab.object_prefix
  * Summary.frozen
  * library_segment

Compilation units

Sourceval start_compilation : Names.DirPath.t -> Names.ModPath.t -> unit

Sourceval end_compilation_checks : Names.DirPath.t -> Libobject.object_name

Source

val end_compilation : 
  Libobject.object_name ->
  Nametab.object_prefix * library_segment

Sourceval library_dp : unit -> Names.DirPath.t

The function library_dp returns the DirPath.t of the current compiling library (or default_library)

Sourceval dp_of_mp : Names.ModPath.t -> Names.DirPath.t

Extract the library part of a name even if in a section

Sourceval split_modpath : Names.ModPath.t -> Names.DirPath.t * Names.Id.t list

Sourceval library_part : Names.GlobRef.t -> Names.DirPath.t

Sections

Sourceval open_section : Names.Id.t -> unit

Sourceval close_section : unit -> unit

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

Sourcetype frozen

Sourceval freeze : unit -> frozen

Sourceval unfreeze : frozen -> unit

Sourceval drop_objects : frozen -> frozen

Keep only the libobject structure, not the objects themselves

Sourceval init : unit -> unit

Sourceval section_segment_of_constant : Names.Constant.t -> Section.abstr_info

Section management for discharge

Sourceval section_segment_of_mutual_inductive : Names.MutInd.t -> Section.abstr_info

Sourceval section_segment_of_reference : Names.GlobRef.t -> Section.abstr_info

Source

val variable_section_segment_of_reference : 
  Names.GlobRef.t ->
  Constr.named_context

Sourceval section_instance : Names.GlobRef.t -> Univ.Instance.t * Names.Id.t array

Sourceval is_in_section : Names.GlobRef.t -> bool

Sourceval replacement_context : unit -> Opaqueproof.work_list

Discharge: decrease the section level if in the current section

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

Source

val discharge_abstract_universe_context : 
  Section.abstr_info ->
  Univ.AUContext.t ->
  Univ.universe_level_subst * Univ.AUContext.t

Object iteration functions.

...

...

...

Functions relative to current path

Modules and module types

Compilation units

Sections

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

Discharge: decrease the section level if in the current section

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