Cooking (u.75d6a066538fb738038ab1b402df0edb.coq.8.14.1.doc.coq-core.kernel.Cooking)

Sourcetype recipe = {

from : Opaqueproof.opaque Declarations.constant_body;
info : Opaqueproof.cooking_info;

}

Sourcetype inline = bool

Sourcetype '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_flags : Declarations.typing_flags;

}

Sourceval cook_constant : recipe -> Opaqueproof.opaque result

Source

val cook_constr : 
  Opaqueproof.cooking_info list ->
  (Constr.constr * unit Opaqueproof.delayed_universes) ->
  Constr.constr * unit Opaqueproof.delayed_universes

Source

val cook_inductive : 
  Opaqueproof.cooking_info ->
  Declarations.mutual_inductive_body ->
  Declarations.mutual_inductive_body

Sourceval expmod_constr : Opaqueproof.work_list -> Constr.constr -> Constr.constr

Module `Cooking`Source

Cooking the constants.

Utility functions used in module `Discharge`.

Cooking the constants.

Utility functions used in module Discharge.

Utility functions used in module `Discharge`.