package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
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
val open_atomic_objects : 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
val segment_of_objects : Nametab.object_prefix -> lib_objects -> library_segment
val add_entry : Libobject.object_name -> node -> unit
val add_anonymous_entry : node -> unit
val add_anonymous_leaf : ?cache_first:bool -> Libobject.obj -> unit
val add_leaves : Names.Id.t -> Libobject.obj list -> Libobject.object_name
val contents : unit -> library_segment
val contents_after : Libobject.object_name -> library_segment
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
val make_kn : Names.Id.t -> Names.KerName.t
val sections_are_opened : unit -> bool
  • deprecated Use Global.sections_are_opened
val sections_depth : unit -> int
val is_module_or_modtype : unit -> bool
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
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
val split_modpath : Names.ModPath.t -> Names.DirPath.t * Names.Id.t list
val library_part : Names.GlobRef.t -> Names.DirPath.t
val open_section : Names.Id.t -> unit
val close_section : unit -> unit
type frozen
val freeze : marshallable:bool -> frozen
val unfreeze : frozen -> unit
val drop_objects : frozen -> frozen
val init : unit -> unit
val section_segment_of_constant : Names.Constant.t -> Section.abstr_info
val section_segment_of_mutual_inductive : Names.MutInd.t -> Section.abstr_info
val section_segment_of_reference : Names.GlobRef.t -> Section.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 -> Opaqueproof.work_list
val discharge_abstract_universe_context : Section.abstr_info -> Univ.AUContext.t -> Univ.universe_level_subst * Univ.AUContext.t
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