Module `Term_typing`

type 'a effect_handler = Environ.env -> Constr.t -> 'a -> Constr.t * Univ.ContextSet.t * int: Handlers are used to manage side-effects. The 'a type stands for the type of side-effects, and it is parametric because they are only defined later on. Handlers inline the provided side-effects into the term, and return the set of additional global constraints that need to be added for the term to be well typed.

type _ trust = | Pure : unit trust | SideEffects : 'a effect_handler -> 'a trust

val translate_local_def : Environ.env -> Names.Id.t -> Entries.section_def_entry -> Constr.constr * Sorts.relevance * Constr.types
val translate_local_assum : Environ.env -> Constr.types -> Constr.types * Sorts.relevance
val translate_constant : 'a trust -> Environ.env -> Names.Constant.t -> 'a Entries.constant_entry -> Declarations.constant_body
val translate_recipe : Environ.env -> Names.Constant.t -> Cooking.recipe -> Declarations.constant_body

val infer_declaration : trust:'a trust -> Environ.env -> 'a Entries.constant_entry -> Cooking.result
val build_constant_declaration : Names.Constant.t -> Environ.env -> Cooking.result -> Declarations.constant_body