package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

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

type is_type = bool
type export = bool option
type 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
type library_segment = (Libobject.object_name * node) list
type lib_atomic_objects = (Names.Id.t * Libobject.obj) list
type lib_objects = (Names.Id.t * Libobject.t) list
Object iteration functions.
val open_atomic_objects : Libobject.open_filter -> int -> Nametab.object_prefix -> lib_atomic_objects -> unit
val load_atomic_objects : int -> Nametab.object_prefix -> lib_atomic_objects -> unit
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.

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

val add_entry : Libobject.object_name -> node -> unit
val add_anonymous_entry : node -> unit
...

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

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

The function contents gives access to the current entire segment

val contents : unit -> library_segment

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

val contents_after : Libobject.object_name -> library_segment
Functions relative to current path
val cwd : unit -> Names.DirPath.t

User-side names

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

  • deprecated Use Global.sections_are_opened
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 current_mod_id : unit -> Names.module_ident
val find_opening_node : Names.Id.t -> node

Returns the opening node of a given name

Modules and module types
Compilation units
val start_compilation : Names.DirPath.t -> Names.ModPath.t -> unit
val end_compilation_checks : Names.DirPath.t -> Libobject.object_name
val 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

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 -> Declarations.abstr_info

Section management for discharge

val section_segment_of_mutual_inductive : Names.MutInd.t -> Declarations.abstr_info
val section_segment_of_reference : Names.GlobRef.t -> Declarations.abstr_info
val variable_section_segment_of_reference : Names.GlobRef.t -> Constr.named_context
val section_instance : Names.GlobRef.t -> Univ.Instance.t * Names.Id.t array
val is_in_section : Names.GlobRef.t -> bool
val replacement_context : unit -> Declarations.work_list
Discharge: decrease the section level if in the current section
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct