package coq
Formal proof management system
Install
dune-project
Dependency
Authors
Maintainers
Sources
coq-8.14.0.tar.gz
sha256=b1501d686c21836302191ae30f610cca57fb309214c126518ca009363ad2cd3c
doc/coq-core.kernel/Cooking/index.html
Module CookingSource
Cooking the constants.
Source
type recipe = {from : Opaqueproof.opaque Declarations.constant_body;info : Opaqueproof.cooking_info;
}Source
type 'opaque result = {cook_body : (Constr.constr, 'opaque) Declarations.constant_def;cook_type : Constr.types;cook_universes : Declarations.universes;cook_relevance : Sorts.relevance;cook_inline : inline;cook_context : Names.Id.Set.t option;cook_flags : Declarations.typing_flags;
}Source
val cook_constr :
Opaqueproof.cooking_info list ->
(Constr.constr * unit Opaqueproof.delayed_universes) ->
Constr.constr * unit Opaqueproof.delayed_universesSource
val cook_inductive :
Opaqueproof.cooking_info ->
Declarations.mutual_inductive_body ->
Declarations.mutual_inductive_body