package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
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 typing_context
val translate_local_assum : Environ.env -> Constr.types -> Constr.types * Sorts.relevance

Internal functions, mentioned here for debug purpose only

val build_constant_declaration : Environ.env -> 'a Cooking.result -> 'a Declarations.pconstant_body