Module ComDefinition
Definitions/Let
val do_definition : program_mode:bool -> ?hook:DeclareDef.Hook.t -> name:Names.Id.t -> scope:DeclareDef.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 interp_definition : program_mode:bool -> Constrexpr.universe_decl_expr option -> Constrexpr.local_binder_expr list -> poly:bool -> Redexpr.red_expr option -> Constrexpr.constr_expr -> Constrexpr.constr_expr option -> Evd.side_effects Declare.proof_entry * Evd.evar_map * UState.universe_decl * Impargs.manual_implicitsNot used anywhere.