Module Cooking

Cooking the constants.
type recipe = {
from : Declarations.constant_body;
info : Opaqueproof.cooking_info;
}
type inline = bool
type result = {
cook_body : Constr.constr Mod_subst.substituted Declarations.constant_def;
cook_type : Constr.types;
cook_universes : Declarations.universes;
cook_private_univs : Univ.ContextSet.t option;
cook_relevance : Sorts.relevance;
cook_inline : inline;
cook_context : Constr.named_context option;
}
val cook_constant : recipe -> result
val cook_constr : Opaqueproof.cooking_info -> Constr.constr -> Constr.constr
Utility functions used in module Discharge.
val expmod_constr : Opaqueproof.work_list -> Constr.constr -> Constr.constr