coq 8.9.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
| OpenedSection of Libnames.object_prefix * Summary.frozen

type 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.ModPath.t

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

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.ModPath.t ->
  Summary.frozen ->
  Libnames.object_prefix

val start_modtype : 
  Names.module_ident ->
  Names.ModPath.t ->
  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.ModPath.t -> 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.ModPath.t -> 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:Summary.marshallable -> frozen

val unfreeze : frozen -> unit

val init : unit -> unit

type variable_info = Constr.named_declaration * Decl_kinds.binding_kind

type variable_context = variable_info list

type abstr_info = private {

abstr_ctx : variable_context;
abstr_subst : Univ.Instance.t;
abstr_uctx : Univ.AUContext.t;

}

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

val named_of_variable_context : variable_context -> Constr.named_context

val section_segment_of_constant : Names.Constant.t -> abstr_info

val section_segment_of_mutual_inductive : Names.MutInd.t -> abstr_info

val section_segment_of_reference : Names.GlobRef.t -> abstr_info

val variable_section_segment_of_reference : Names.GlobRef.t -> variable_context

val section_instance : Names.GlobRef.t -> Univ.Instance.t * Names.Id.t array

val is_in_section : Names.GlobRef.t -> bool

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

val add_section_context : Univ.ContextSet.t -> unit

val add_section_constant : 
  Decl_kinds.polymorphic ->
  Names.Constant.t ->
  Constr.named_context ->
  unit

val add_section_kn : 
  Decl_kinds.polymorphic ->
  Names.MutInd.t ->
  Constr.named_context ->
  unit

val replacement_context : unit -> Opaqueproof.work_list

val discharge_kn : Names.MutInd.t -> Names.MutInd.t

val discharge_con : Names.Constant.t -> Names.Constant.t

val discharge_proj_repr : Names.Projection.Repr.t -> Names.Projection.Repr.t

val discharge_global : Names.GlobRef.t -> Names.GlobRef.t

val discharge_inductive : Names.inductive -> Names.inductive

val discharge_abstract_universe_context : 
  abstr_info ->
  Univ.AUContext.t ->
  Univ.universe_level_subst * Univ.AUContext.t

package coq