Module `ComDefinition`

val do_definition : ?⁠hook:Declare.Hook.t -> name:Names.Id.t -> scope:Declare.locality -> poly:bool -> kind:Decls.definition_object_kind -> 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 -> name:Names.Id.t -> scope:Declare.locality -> poly:bool -> kind:Decls.definition_object_kind -> Constrexpr.universe_decl_expr option -> Constrexpr.local_binder_expr list -> Redexpr.red_expr option -> Constrexpr.constr_expr -> Constrexpr.constr_expr option -> unit