From 9923a8d9f8ca0c411d01d0790439ff02dc9dab8c Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Thu, 4 Sep 2025 23:08:45 -0700
Subject: [PATCH] chore: remove special case for `extern` constructors (#10257)

This is subsumed by the fix in #10256.
---
 src/Lean/Compiler/IR/ToIR.lean | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/src/Lean/Compiler/IR/ToIR.lean b/src/Lean/Compiler/IR/ToIR.lean
index 754d87d674..67d5ebfa7c 100644
--- a/src/Lean/Compiler/IR/ToIR.lean
+++ b/src/Lean/Compiler/IR/ToIR.lean
@@ -160,9 +160,6 @@ partial def lowerLet (decl : LCNF.LetDecl) (k : LCNF.Code) : M FnBody := do
     let env ← Lean.getEnv
     match env.find? name with
     | some (.ctorInfo ctorVal) =>
-      if isExtern env name then
-        return (← mkFap name irArgs)
-
       let type ← nameToIRType ctorVal.induct
       if type.isScalar then
         let var ← bindVar decl.fvarId