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 : 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
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 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 : unit -> 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