From c9e902034d3db140d171680ced01af002df10f9e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 21 Sep 2020 11:44:26 -0700
Subject: [PATCH] fix: typo

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

diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index 9e766d9a12..1d83843d01 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -519,7 +519,7 @@ partial def importModulesAux : List Import → (NameSet × Array ModuleData × A
     let regions := regions.push region;
     importModulesAux is (s, mods, regions)
 
-private partial def getEntriesFor (mod : ModuleData) (extId : Name) : Nat → Array EnvExtensionState
+private partial def getEntriesFor (mod : ModuleData) (extId : Name) : Nat → Array EnvExtensionEntry
 | i =>
   if i < mod.entries.size then
     let curr := mod.entries.get! i;