diff --git a/stage0/src/Init/LeanInit.lean b/stage0/src/Init/LeanInit.lean
index 6bed75569d..557893b12d 100644
--- a/stage0/src/Init/LeanInit.lean
+++ b/stage0/src/Init/LeanInit.lean
@@ -83,6 +83,13 @@ mkNameStr Name.anonymous s
 
 namespace Name
 
+@[extern "lean_name_eq"]
+protected def beq : (@& Name) → (@& Name) → Bool
+| anonymous,   anonymous   => true
+| str p₁ s₁ _, str p₂ s₂ _ => s₁ == s₂ && beq p₁ p₂
+| num p₁ n₁ _, num p₂ n₂ _ => n₁ == n₂ && beq p₁ p₂
+| _,           _           => false
+
 @[extern "lean_name_eq"]
 protected def Name.beq : (@& Name) → (@& Name) → Bool
 | anonymous,   anonymous   => true
diff --git a/stage0/src/library/compiler/compiler.cpp b/stage0/src/library/compiler/compiler.cpp
index 8ad87ceb26..1e3f3ff8a3 100644
--- a/stage0/src/library/compiler/compiler.cpp
+++ b/stage0/src/library/compiler/compiler.cpp
@@ -173,13 +173,16 @@ environment compile(environment const & env, options const & opts, names cs) {
         }
     }
 
-    if (length(cs) == 1 && is_extern_constant(env, head(cs))) {
-        /* Generate boxed version for extern/native constant if needed. */
-        return ir::add_extern(env, head(cs));
+    if (length(cs) == 1) {
+        name c = get_real_name(head(cs));
+        if (is_extern_constant(env, c)) {
+            /* Generate boxed version for extern/native constant if needed. */
+            return ir::add_extern(env, c);
+        }
     }
 
     for (name const & c : cs) {
-        lean_assert(!is_extern_constant(env, c));
+        lean_assert(!is_extern_constant(env, get_real_name(c)));
         constant_info cinfo = env.get(c);
         if (!cinfo.is_definition() && !cinfo.is_opaque()) return env;
         if (has_synthetic_sorry(cinfo)) return env;
diff --git a/stage0/stdlib/Init/LeanInit.c b/stage0/stdlib/Init/LeanInit.c
index e4a70fe349..a86f770363 100644
--- a/stage0/stdlib/Init/LeanInit.c
+++ b/stage0/stdlib/Init/LeanInit.c
@@ -91,6 +91,7 @@ uint8_t l_Char_isDigit(uint32_t);
 lean_object* l_Lean_charLitKind___closed__2;
 lean_object* l_Lean_Substring_HasQuote(lean_object*);
 lean_object* l___private_Init_LeanInit_8__decodeOctalLitAux___boxed(lean_object*, lean_object*, lean_object*);
+uint8_t lean_name_eq(lean_object*, lean_object*);
 lean_object* l___private_Init_LeanInit_8__decodeOctalLitAux(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_isGreek___boxed(lean_object*);
 lean_object* l_Lean_Substring_HasQuote___closed__2;
@@ -341,6 +342,7 @@ lean_object* l_Lean_Name_append(lean_object*, lean_object*);
 uint8_t l_Lean_isGreek(uint32_t);
 lean_object* l_Lean_Syntax_getKind(lean_object*);
 lean_object* l_Lean_MacroScopesView_review(lean_object*);
+lean_object* l_Lean_Name_beq___boxed(lean_object*, lean_object*);
 lean_object* l_Lean_Syntax_getArg___boxed(lean_object*, lean_object*);
 lean_object* l_Array_filterSepElems(lean_object*, lean_object*);
 lean_object* l_Array_mapSepElemsM___at_Array_mapSepElems___spec__1(lean_object*, lean_object*);
@@ -1215,6 +1217,17 @@ x_3 = lean_name_mk_string(x_2, x_1);
 return x_3;
 }
 }
+lean_object* l_Lean_Name_beq___boxed(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+uint8_t x_3; lean_object* x_4; 
+x_3 = lean_name_eq(x_1, x_2);
+lean_dec(x_2);
+lean_dec(x_1);
+x_4 = lean_box(x_3);
+return x_4;
+}
+}
 lean_object* l_Lean_Name_Name_beq___boxed(lean_object* x_1, lean_object* x_2) {
 _start:
 {