diff --git a/src/library/compiler/specialize.cpp b/src/library/compiler/specialize.cpp index 515836dfa5..f661339392 100644 --- a/src/library/compiler/specialize.cpp +++ b/src/library/compiler/specialize.cpp @@ -1020,8 +1020,12 @@ pair specialize(environment env, comp_decls const & ds, comp_decls r; for (comp_decl const & d : ds) { comp_decls new_ds; - std::tie(env, new_ds) = specialize_core(env, d, cfg); - r = append(r, new_ds); + if (has_specialize_attribute(env, d.fst())) { + r = append(r, comp_decls(d)); + } else { + std::tie(env, new_ds) = specialize_core(env, d, cfg); + r = append(r, new_ds); + } } return mk_pair(env, r); }