package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.17.1.tar.gz
sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b
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 ->
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 ->
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