Constant_typingtype 'a effect_handler = Environ.env -> Constr.t -> 'a -> Constr.t * Univ.ContextSet.t * intHandlers 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.
val infer_local_def : Environ.env -> Names.Id.t -> Entries.section_def_entry -> Constr.constr * Sorts.relevance * Constr.typesval infer_local_assum : Environ.env -> Constr.types -> Constr.types * Sorts.relevanceval infer_primitive : Environ.env -> Entries.primitive_entry -> ('a, unit) Declarations.pconstant_bodyval infer_symbol : Environ.env -> Entries.symbol_entry -> ('a, unit) Declarations.pconstant_bodyval infer_parameter : sec_univs:UVars.Instance.t option -> Environ.env -> Entries.parameter_entry -> ('a, unit) Declarations.pconstant_bodyval infer_definition : sec_univs:UVars.Instance.t option -> Environ.env -> Entries.definition_entry -> HConstr.t option * ('a, unit) Declarations.pconstant_bodyval infer_opaque : sec_univs:UVars.Instance.t option -> Environ.env -> 'a Entries.opaque_entry -> (unit, unit) Declarations.pconstant_body * typing_contextval check_delayed : 'a effect_handler -> typing_context -> 'a Entries.proof_output -> HConstr.t option * Constr.t * Univ.ContextSet.t Opaqueproof.delayed_universes