package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
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 named_context_val : unit -> Environ.named_context_val
val named_context : unit -> Constr.named_context
val set_engagement : Declarations.engagement -> unit
val set_typing_flags : Declarations.typing_flags -> unit
val typing_flags : unit -> Declarations.typing_flags
val push_named_assum : (Names.Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit
val push_named_def : (Names.Id.t * Entries.section_def_entry) -> unit
val add_constraints : Univ.Constraint.t -> unit
val push_context : bool -> Univ.UContext.t -> unit
val push_context_set : bool -> Univ.ContextSet.t -> unit
val start_module : Names.Id.t -> Names.ModPath.t
val start_modtype : Names.Id.t -> Names.ModPath.t
val end_modtype : Summary.frozen -> Names.Id.t -> Names.ModPath.t * Names.MBId.t list
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 : Names.Constant.t -> (Constr.constr * Univ.AUContext.t) option
val body_of_constant_body : Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option
val start_library : Names.DirPath.t -> 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_type_in_type : Names.GlobRef.t -> bool
val constr_of_global_in_context : Environ.env -> Names.GlobRef.t -> Constr.types * Univ.AUContext.t
val type_of_global_in_context : Environ.env -> Names.GlobRef.t -> Constr.types * Univ.AUContext.t
val universes_of_global : Names.GlobRef.t -> Univ.AUContext.t
val register : Retroknowledge.field -> Constr.constr -> Constr.constr -> unit
val register_inline : Names.Constant.t -> unit
val set_strategy : Names.Constant.t Names.tableKey -> Conv_oracle.level -> unit
val set_reduction_sharing : 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