package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type side_effects
type !_ trust =
  1. | Pure : unit trust
  2. | SideEffects : Declarations.structure_body -> side_effects trust
val translate_local_assum : Environ.env -> Constr.types -> Constr.types
val inline_side_effects : Environ.env -> Constr.constr -> side_effects -> Constr.constr
val empty_seff : side_effects
val concat_seff : side_effects -> side_effects -> side_effects
val uniq_seff : side_effects -> Entries.side_effect list
val equal_eff : Entries.side_effect -> Entries.side_effect -> bool
type side_effect_role =
  1. | Subproof
  2. | Schema of Names.inductive * string
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.