Dischargeval cook_opaque_proofterm :
Cooking.cooking_info list ->
Opaqueproof.opaque_proofterm ->
Opaqueproof.opaque_prooftermval cook_constant :
Environ.env ->
Cooking.cooking_info ->
Declarations.constant_body ->
Declarations.constant_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