Module `ComDefinition`

val do_definition : ontop:Proof_global.t option -> program_mode:bool -> ?⁠hook:Lemmas.declaration_hook -> Names.Id.t -> Decl_kinds.definition_kind -> Constrexpr.universe_decl_expr option -> Constrexpr.local_binder_expr list -> Redexpr.red_expr option -> Constrexpr.constr_expr -> Constrexpr.constr_expr option -> unit

val interp_definition : program_mode:bool -> Constrexpr.universe_decl_expr option -> Constrexpr.local_binder_expr list -> Decl_kinds.polymorphic -> Redexpr.red_expr option -> Constrexpr.constr_expr -> Constrexpr.constr_expr option -> Safe_typing.private_constants Entries.definition_entry * Evd.evar_map * UState.universe_decl * Impargs.manual_implicits: Not used anywhere.