Module Cooking

Cooking the constants.
type recipe = {
from : Opaqueproof.opaque Declarations.constant_body;
info : Opaqueproof.cooking_info;
}
type inline = bool
type 'opaque result = {
cook_body : (Constr.constr Mod_subst.substituted, '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;
}
val cook_constant : recipe -> Opaqueproof.opaque result
val cook_constr : Opaqueproof.cooking_info list -> (Constr.constr * unit Opaqueproof.delayed_universes) -> Constr.constr * unit Opaqueproof.delayed_universes
val cook_inductive : Opaqueproof.cooking_info -> Declarations.mutual_inductive_body -> Entries.mutual_inductive_entry
Utility functions used in module Discharge.
val expmod_constr : Opaqueproof.work_list -> Constr.constr -> Constr.constr