package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type !'a effect_handler = Environ.env -> Constr.t -> 'a -> Constr.t * Univ.ContextSet.t * int
type !_ trust =
  1. | Pure : unit trust
  2. | SideEffects : 'a effect_handler -> 'a trust
val translate_local_assum : Environ.env -> Constr.types -> Constr.types * Sorts.relevance
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
OCaml

Innovation. Community. Security.