package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
type section_variable_entry =
  1. | SectionLocalDef of Safe_typing.private_constants Entries.definition_entry
  2. | SectionLocalAssum of Constr.types Univ.in_universe_context_set * Decl_kinds.polymorphic * bool
type internal_flag =
  1. | UserAutomaticRequest
  2. | InternalTacticRequest
  3. | UserIndividualRequest
val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool -> ?inline:bool -> ?types:Constr.types -> ?univs:Entries.universes_entry -> ?eff:Safe_typing.private_constants -> Constr.constr -> Safe_typing.private_constants Entries.definition_entry
val declare_constant : ?internal:internal_flag -> ?local:bool -> Names.Id.t -> ?export_seff:bool -> constant_declaration -> Names.Constant.t
val declare_definition : ?internal:internal_flag -> ?opaque:bool -> ?kind:Decl_kinds.definition_object_kind -> ?local:bool -> Names.Id.t -> ?types:Constr.constr -> Constr.constr Entries.in_universes_entry -> Names.Constant.t
val set_declare_scheme : (string -> (Names.inductive * Names.Constant.t) array -> unit) -> unit
val definition_message : Names.Id.t -> unit
val assumption_message : Names.Id.t -> unit
val fixpoint_message : int array option -> Names.Id.t list -> unit
val cofixpoint_message : Names.Id.t list -> unit
val recursive_message : bool -> int array option -> Names.Id.t list -> unit
val exists_name : Names.Id.t -> bool
val declare_univ_binders : Names.GlobRef.t -> UnivNames.universe_binders -> unit
val declare_universe_context : Decl_kinds.polymorphic -> Univ.ContextSet.t -> unit
val do_universe : Decl_kinds.polymorphic -> Names.lident list -> unit
OCaml

Innovation. Community. Security.