coq 8.7.1 · OCaml Package

coq

type is_type = bool

type export = bool option

type node =

| Leaf of Libobject.obj
| CompilingLibrary of Libnames.object_prefix
| OpenedModule of is_type * export * Libnames.object_prefix * Summary.frozen
| ClosedModule of library_segment
| OpenedSection of Libnames.object_prefix * Summary.frozen
| ClosedSection of library_segment

and library_segment = (Libnames.object_name * node) list

type lib_objects = (Names.Id.t * Libobject.obj) list

val open_objects : int -> Libnames.object_prefix -> lib_objects -> unit

val load_objects : int -> Libnames.object_prefix -> lib_objects -> unit

val subst_objects : Mod_subst.substitution -> lib_objects -> lib_objects

val classify_segment : 
  library_segment ->
  lib_objects * lib_objects * Libobject.obj list

val segment_of_objects : 
  Libnames.object_prefix ->
  lib_objects ->
  library_segment

val add_leaf : Names.Id.t -> Libobject.obj -> Libnames.object_name

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

val pull_to_head : Libnames.object_name -> unit

val add_leaves : Names.Id.t -> Libobject.obj list -> Libnames.object_name

val contents : unit -> library_segment

val contents_after : Libnames.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.module_path

val make_kn : Names.Id.t -> Names.kernel_name

val sections_are_opened : unit -> bool

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_module : 
  export ->
  Names.module_ident ->
  Names.module_path ->
  Summary.frozen ->
  Libnames.object_prefix

val start_modtype : 
  Names.module_ident ->
  Names.module_path ->
  Summary.frozen ->
  Libnames.object_prefix

val end_module : 
  unit ->
  Libnames.object_name
  * Libnames.object_prefix
  * Summary.frozen
  * library_segment

val end_modtype : 
  unit ->
  Libnames.object_name
  * Libnames.object_prefix
  * Summary.frozen
  * library_segment

val start_compilation : Names.DirPath.t -> Names.module_path -> unit

val end_compilation_checks : Names.DirPath.t -> Libnames.object_name

val end_compilation : 
  Libnames.object_name ->
  Libnames.object_prefix * library_segment

val library_dp : unit -> Names.DirPath.t

val dp_of_mp : Names.module_path -> Names.DirPath.t

val split_modpath : Names.module_path -> Names.DirPath.t * Names.Id.t list

val library_part : Globnames.global_reference -> Names.DirPath.t

val open_section : Names.Id.t -> unit

val close_section : unit -> unit

type frozen

val freeze : marshallable:Summary.marshallable -> frozen

val unfreeze : frozen -> unit

val init : unit -> unit

val xml_open_section : (Names.Id.t -> unit) Hook.t

val xml_close_section : (Names.Id.t -> unit) Hook.t

type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind

type variable_context = variable_info list

type abstr_info =
  variable_context * Univ.universe_level_subst * Univ.AUContext.t

val instance_from_variable_context : variable_context -> Names.Id.t array

val named_of_variable_context : variable_context -> Context.Named.t

val section_segment_of_constant : Names.constant -> abstr_info

val section_segment_of_mutual_inductive : Names.mutual_inductive -> abstr_info

val variable_section_segment_of_reference : 
  Globnames.global_reference ->
  variable_context

val section_instance : 
  Globnames.global_reference ->
  Univ.universe_instance * Names.Id.t array

val is_in_section : Globnames.global_reference -> bool

val add_section_variable : 
  Names.Id.t ->
  Decl_kinds.binding_kind ->
  Decl_kinds.polymorphic ->
  Univ.universe_context_set ->
  unit

val add_section_context : Univ.universe_context_set -> unit

val add_section_constant : 
  Decl_kinds.polymorphic ->
  Names.constant ->
  Context.Named.t ->
  unit

val add_section_kn : 
  Decl_kinds.polymorphic ->
  Names.mutual_inductive ->
  Context.Named.t ->
  unit

val replacement_context : unit -> Opaqueproof.work_list

val discharge_kn : Names.mutual_inductive -> Names.mutual_inductive

val discharge_con : Names.constant -> Names.constant

val discharge_global : Globnames.global_reference -> Globnames.global_reference

val discharge_inductive : Names.inductive -> Names.inductive

package coq