Module Discharge

type inline = bool
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_univ_hyps : Univ.Instance.t;
cook_flags : Declarations.typing_flags;
}
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