Dischargeval cook_opaque_proofterm : Cooking.cooking_info list -> Opaqueproof.opaque_proofterm -> Opaqueproof.opaque_prooftermval cook_constant : Environ.env -> Cooking.cooking_info -> Declarations.constant_body -> (Opaqueproof.opaque, unit) Declarations.pconstant_bodyval cook_inductive : Cooking.cooking_info -> Declarations.mutual_inductive_body -> Declarations.mutual_inductive_bodyval cook_rel_context : Cooking.cooking_info -> Constr.rel_context -> Constr.rel_context