package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.18.0.tar.gz
md5=8d852367b54f095d9fbabd000304d450
sha512=46922d5f2eb6802a148a52fd3e7f0be8370c93e7bc33cee05cf4a2044290845b10ccddbaa306f29c808e7c5019700763e37e45ff6deb507b874a4348010fed50
doc/coq-core.vernac/ComAssumption/index.html
Module ComAssumptionSource
Parameters/Assumptions
Source
val interp_assumption :
program_mode:bool ->
Environ.env ->
Evd.evar_map ->
Constrintern.internalization_env ->
Constrexpr.local_binder_expr list ->
Constrexpr.constr_expr ->
Evd.evar_map * EConstr.t * Impargs.manual_implicitsSource
val do_assumptions :
program_mode:bool ->
poly:bool ->
scope:Locality.definition_scope ->
kind:Decls.assumption_object_kind ->
?deprecation:Deprecation.t ->
Declaremods.inline ->
(Constrexpr.ident_decl list * Constrexpr.constr_expr)
Vernacexpr.with_coercion
list ->
unitSource
val declare_variable :
Vernacexpr.coercion_flag ->
kind:Decls.assumption_object_kind ->
Constr.types ->
UState.named_universes_entry ->
Impargs.manual_implicits ->
Glob_term.binding_kind ->
Names.variable CAst.t ->
unitSource
val declare_axiom :
Vernacexpr.coercion_flag ->
poly:bool ->
local:Locality.import_status ->
kind:Decls.assumption_object_kind ->
?deprecation:Deprecation.t ->
Constr.types ->
UState.named_universes_entry ->
Impargs.manual_implicits ->
Declaremods.inline ->
Names.variable CAst.t ->
Names.GlobRef.t * Univ.Instance.tContext command
Source
val interp_context :
Environ.env ->
Evd.evar_map ->
Constrexpr.local_binder_expr list ->
Evd.evar_map
* (Names.Id.t * Constr.t option * Constr.t * Glob_term.binding_kind) listThe first half of the context command, from expr to constr
On This Page