From 91a2de1e1e121aaf5570cbc3c461de985fe5880d Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Fri, 22 Aug 2025 21:07:23 -0700
Subject: [PATCH] chore: use `forallTelescope` rather than
 `forallTelescopeReducing` (#10073)

---
 src/Lean/Compiler/IR/ToIRType.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Compiler/IR/ToIRType.lean b/src/Lean/Compiler/IR/ToIRType.lean
index 3cf47d993c..68cd8e3548 100644
--- a/src/Lean/Compiler/IR/ToIRType.lean
+++ b/src/Lean/Compiler/IR/ToIRType.lean
@@ -63,7 +63,7 @@ where fillCache : CoreM IRType := do
       for ctorName in ctorNames do
         let some (.ctorInfo ctorInfo) := env.find? ctorName | unreachable!
         let hasRelevantField ← Meta.MetaM.run' <|
-                               Meta.forallTelescopeReducing ctorInfo.type fun params _ => do
+                               Meta.forallTelescope ctorInfo.type fun params _ => do
           for field in params[ctorInfo.numParams...*] do
             let fieldType ← field.fvarId!.getType
             let lcnfFieldType ← LCNF.toLCNFType fieldType