From 049ff2b0221568acb71d638acbe2bf7abe2664aa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 25 Sep 2020 11:16:52 -0700 Subject: [PATCH] fix: bad message --- src/Lean/Compiler/Specialize.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Compiler/Specialize.lean b/src/Lean/Compiler/Specialize.lean index e5b4a9fc09..5626752321 100644 --- a/src/Lean/Compiler/Specialize.lean +++ b/src/Lean/Compiler/Specialize.lean @@ -27,8 +27,8 @@ end SpecializeAttributeKind def mkSpecializeAttrs : IO (EnumAttributes SpecializeAttributeKind) := registerEnumAttributes `specializeAttrs - [(`specialize, "mark definition to always be inlined", SpecializeAttributeKind.specialize), - (`nospecialize, "mark definition to never be inlined", SpecializeAttributeKind.nospecialize) ] + [(`specialize, "mark definition to always be specialized", SpecializeAttributeKind.specialize), + (`nospecialize, "mark definition to never be specialized", SpecializeAttributeKind.nospecialize) ] /- TODO: fix the following hack. We need to use the following hack because the equation compiler generates auxiliary definitions that are compiled before we even finish the elaboration of the current command.