package coq-core
Module DischargeSource
Source
val cook_opaque_proofterm :
Cooking.cooking_info list ->
Opaqueproof.opaque_proofterm ->
Opaqueproof.opaque_prooftermSource
val cook_constant :
Environ.env ->
Cooking.cooking_info ->
Declarations.constant_body ->
(Opaqueproof.opaque, unit) Declarations.pconstant_bodySource
val cook_inductive :
Cooking.cooking_info ->
Declarations.mutual_inductive_body ->
Declarations.mutual_inductive_body