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.proofs/Logic/index.html
Module LogicSource
Legacy proof engine. Do not use in newly written code.
check respectively means:\\ Intro: check that the name does not exist\\ Intro_after: check that the name does not exist and that variables in its type does not escape their scope\\ Intro_replacing: check that the name does not exist and that variables in its type does not escape their scope\\ Convert_hyp: check that the name exist and that its type is convertible\\
Refiner errors.
Source
type refiner_error = | BadType of Constr.constr * Constr.constr * EConstr.t| UnresolvedBindings of Names.Name.t list| CannotApply of Constr.constr * Constr.constr| NonLinearProof of Constr.constr| MetaInType of EConstr.constr| IntroNeedsProduct| NoSuchHyp of Names.Id.t
Move destination for hypothesis
Source
val convert_hyp :
check:bool ->
reorder:bool ->
Environ.env ->
Evd.evar_map ->
EConstr.named_declaration ->
Environ.named_context_valSource
val move_hyp_in_named_context :
Environ.env ->
Evd.evar_map ->
Names.Id.t ->
Names.Id.t move_location ->
Environ.named_context_val ->
Environ.named_context_valSource
val insert_decl_in_named_context :
Environ.env ->
Evd.evar_map ->
EConstr.named_declaration ->
Names.Id.t move_location ->
Environ.named_context_val ->
Environ.named_context_valOn This Page