package coq-core

  1. Overview
  2. Docs
On This Page
  1. Definitions/Let
Legend:
Library
Module
Module type
Parameter
Class
Class type
Definitions/Let
val do_definition : ?hook:Declare.Hook.t -> name:Names.Id.t -> ?scope:Locality.definition_scope -> ?clearbody:bool -> poly:bool -> ?typing_flags:Declarations.typing_flags -> kind:Decls.definition_object_kind -> ?using:Vernacexpr.section_subset_expr -> ?user_warns:UserWarn.t -> Constrexpr.universe_decl_expr option -> Constrexpr.local_binder_expr list -> Redexpr.red_expr option -> Constrexpr.constr_expr -> Constrexpr.constr_expr option -> unit
val do_definition_program : ?hook:Declare.Hook.t -> pm:Declare.OblState.t -> name:Names.Id.t -> scope:Locality.definition_scope -> ?clearbody:bool -> poly:bool -> ?typing_flags:Declarations.typing_flags -> kind:Decls.logical_kind -> ?using:Vernacexpr.section_subset_expr -> ?user_warns:UserWarn.t -> Constrexpr.universe_decl_expr option -> Constrexpr.local_binder_expr list -> Redexpr.red_expr option -> Constrexpr.constr_expr -> Constrexpr.constr_expr option -> Declare.OblState.t
OCaml

Innovation. Community. Security.