package coq

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module LibSource

Lib: record of operations, backtrack, low-level sections

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
Sourcetype node =
  1. | Leaf of Libobject.t
  2. | CompilingLibrary of Nametab.object_prefix
  3. | OpenedModule of is_type * export * Nametab.object_prefix * Summary.frozen
  4. | 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.
Sourceval open_atomic_objects : Libobject.open_filter -> int -> Nametab.object_prefix -> lib_atomic_objects -> unit
Sourceval load_atomic_objects : int -> Nametab.object_prefix -> lib_atomic_objects -> unit
Sourceval 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.

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_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.

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_except_section : Names.Id.t -> Libnames.full_path
Sourceval current_mp : unit -> Names.ModPath.t

Kernel-side names

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
Compilation units
Sourceval start_compilation : Names.DirPath.t -> Names.ModPath.t -> unit
Sourceval end_compilation_checks : Names.DirPath.t -> Libobject.object_name
Sourceval library_dp : unit -> Names.DirPath.t

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

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
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
Sourceval 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
OCaml

Innovation. Community. Security.