package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.19.2.tar.gz
md5=5d1187d5e44ed0163f76fb12dabf012e
sha512=91bc81530fa4f6498961583ad51eac5001f139881788b88e360a866ad8e2a6e2c5bce86d1a580ab4cd4782bf49d48318767df82471ce33ba3ac143e5569ad33c
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 ->
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 * UVars.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