Module `Discharge`

val cook_opaque_proofterm : Cooking.cooking_info list -> Opaqueproof.opaque_proofterm -> Opaqueproof.opaque_proofterm
val cook_constant : Environ.env -> Cooking.cooking_info -> Declarations.constant_body -> Declarations.constant_body
val cook_inductive : Cooking.cooking_info -> Declarations.mutual_inductive_body -> Declarations.mutual_inductive_body
val cook_rel_context : Cooking.cooking_info -> Constr.rel_context -> Constr.rel_context