package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.19.0.tar.gz
md5=64b49dbc3205477bd7517642c0b9cbb6
sha512=02fb5b4fb575af79e092492cbec6dc0d15a1d74a07f827f657a72d4e6066532630e5a6d15be4acdb73314bd40b9a321f9ea0584e0ccfe51fd3a56353bd30db9b
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