package coq

  1. Overview
  2. Docs
package coq
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 inline_entry_side_effects : Environ.env -> side_effects Entries.definition_entry -> unit Entries.definition_entry
val empty_seff : side_effects
val concat_seff : side_effects -> side_effects -> side_effects
val uniq_seff : side_effects -> Entries.side_eff list
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