coq 8.11.0 · OCaml Package

coq

val safe_env : unit -> Safe_typing.safe_environment

val env : unit -> Environ.env

val env_is_initial : unit -> bool

val universes : unit -> UGraph.t

val universes_lbound : unit -> Univ.Level.t

val named_context_val : unit -> Environ.named_context_val

val named_context : unit -> Constr.named_context

val set_engagement : Declarations.engagement -> unit

val set_indices_matter : bool -> unit

val set_typing_flags : Declarations.typing_flags -> unit

val set_check_guarded : bool -> unit

val set_check_positive : bool -> unit

val set_check_universes : bool -> unit

val typing_flags : unit -> Declarations.typing_flags

val make_sprop_cumulative : unit -> unit

val set_allow_sprop : bool -> unit

val sprop_allowed : unit -> bool

val push_named_assum : (Names.Id.t * Constr.types) -> unit

val push_named_def : (Names.Id.t * Entries.section_def_entry) -> unit

val push_section_context : (Names.Name.t array * Univ.UContext.t) -> unit

val export_private_constants : 
  Safe_typing.private_constants Entries.proof_output ->
  Constr.constr Univ.in_universe_context_set
  * Safe_typing.exported_private_constant list

val add_constant : 
  Names.Id.t ->
  Safe_typing.global_declaration ->
  Names.Constant.t

val add_private_constant : 
  Names.Id.t ->
  Safe_typing.side_effect_declaration ->
  Names.Constant.t * Safe_typing.private_constants

val add_mind : Names.Id.t -> Entries.mutual_inductive_entry -> Names.MutInd.t

val add_constraints : Univ.Constraint.t -> unit

val push_context_set : bool -> Univ.ContextSet.t -> unit

val add_module : 
  Names.Id.t ->
  Entries.module_entry ->
  Declarations.inline ->
  Names.ModPath.t * Mod_subst.delta_resolver

val add_modtype : 
  Names.Id.t ->
  Entries.module_type_entry ->
  Declarations.inline ->
  Names.ModPath.t

val add_include : 
  Entries.module_struct_entry ->
  bool ->
  Declarations.inline ->
  Mod_subst.delta_resolver

val open_section : unit -> unit

val close_section : Summary.frozen -> unit

val sections_are_opened : unit -> bool

val start_module : Names.Id.t -> Names.ModPath.t

val start_modtype : Names.Id.t -> Names.ModPath.t

val end_module : 
  Summary.frozen ->
  Names.Id.t ->
  (Entries.module_struct_entry * Declarations.inline) option ->
  Names.ModPath.t * Names.MBId.t list * Mod_subst.delta_resolver

val end_modtype : 
  Summary.frozen ->
  Names.Id.t ->
  Names.ModPath.t * Names.MBId.t list

val add_module_parameter : 
  Names.MBId.t ->
  Entries.module_struct_entry ->
  Declarations.inline ->
  Mod_subst.delta_resolver

val lookup_named : Names.variable -> Constr.named_declaration

val lookup_constant : 
  Names.Constant.t ->
  Opaqueproof.opaque Declarations.constant_body

val lookup_inductive : 
  Names.inductive ->
  Declarations.mutual_inductive_body * Declarations.one_inductive_body

val lookup_pinductive : 
  Constr.pinductive ->
  Declarations.mutual_inductive_body * Declarations.one_inductive_body

val lookup_mind : Names.MutInd.t -> Declarations.mutual_inductive_body

val lookup_module : Names.ModPath.t -> Declarations.module_body

val lookup_modtype : Names.ModPath.t -> Declarations.module_type_body

val exists_objlabel : Names.Label.t -> bool

val constant_of_delta_kn : Names.KerName.t -> Names.Constant.t

val mind_of_delta_kn : Names.KerName.t -> Names.MutInd.t

val opaque_tables : unit -> Opaqueproof.opaquetab

val body_of_constant : 
  Opaqueproof.indirect_accessor ->
  Names.Constant.t ->
  (Constr.constr * unit Opaqueproof.delayed_universes * Univ.AUContext.t)
    option

val body_of_constant_body : 
  Opaqueproof.indirect_accessor ->
  Opaqueproof.opaque Declarations.constant_body ->
  (Constr.constr * unit Opaqueproof.delayed_universes * Univ.AUContext.t)
    option

val start_library : Names.DirPath.t -> Names.ModPath.t

val export : 
  ?except:Future.UUIDSet.t ->
  output_native_objects:bool ->
  Names.DirPath.t ->
  Names.ModPath.t * Safe_typing.compiled_library * Safe_typing.native_library

val import : 
  Safe_typing.compiled_library ->
  Univ.ContextSet.t ->
  Safe_typing.vodigest ->
  Names.ModPath.t

val env_of_context : Environ.named_context_val -> Environ.env

val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit

val is_joined_environment : unit -> bool

val is_polymorphic : Names.GlobRef.t -> bool

val is_template_polymorphic : Names.GlobRef.t -> bool

val is_template_checked : Names.GlobRef.t -> bool

val get_template_polymorphic_variables : Names.GlobRef.t -> Univ.Level.t list

val is_type_in_type : Names.GlobRef.t -> bool

val register_inline : Names.Constant.t -> unit

val register_inductive : Names.inductive -> 'a CPrimitives.prim_ind -> unit

val set_strategy : Names.Constant.t Names.tableKey -> Conv_oracle.level -> unit

val set_share_reduction : bool -> unit

val set_VM : bool -> unit

val set_native_compiler : bool -> unit

val current_modpath : unit -> Names.ModPath.t

val current_dirpath : unit -> Names.DirPath.t

val with_global : 
  (Environ.env -> Names.DirPath.t -> 'a Univ.in_universe_context_set) ->
  'a

val global_env_summary_tag : Safe_typing.safe_environment Summary.Dyn.tag

package coq