package coq

  1. Overview
  2. Docs
package coq
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_flag =
  1. | Export
  2. | Import
Sourcetype export = (export_flag * Libobject.open_filter) option
Sourcetype node =
  1. | CompilingLibrary of Nametab.object_prefix
  2. | OpenedModule of is_type * export * Nametab.object_prefix * Summary.frozen
  3. | OpenedSection of Nametab.object_prefix * Summary.frozen
Sourceval 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.

Sourcetype library_segment = (node * Libobject.t list) list
Sourcetype classified_objects = {
  1. substobjs : Libobject.t list;
  2. keepobjs : Libobject.t list;
  3. anticipateobjs : Libobject.t list;
}
...

Low-level adding operations (does not cache)

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

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

Sourceval add_leaf : Libobject.obj -> unit
...

The function contents gives access to the current entire segment

Sourceval contents : unit -> library_segment
Functions relative to current path
Sourceval prefix : unit -> Nametab.object_prefix

User-side names

Sourceval cwd : unit -> Names.DirPath.t
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 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 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 -> Cooking.cooking_info

Section management for discharge

Sourceval section_segment_of_inductive : Names.MutInd.t -> Cooking.cooking_info
Sourceval section_segment_of_reference : Names.GlobRef.t -> Cooking.cooking_info
Sourceval section_instance : Names.GlobRef.t -> Constr.t array
Sourceval is_in_section : Names.GlobRef.t -> bool
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