From 5e2111f4a4e47a3bc59e948b90cbbb4d4bd7f855 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 14 May 2019 12:53:50 -0700 Subject: [PATCH] fix(library/init/lean/environment): process entries using the order they were inserted --- library/init/lean/environment.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/init/lean/environment.lean b/library/init/lean/environment.lean index 8d8b218768..326e708b3e 100644 --- a/library/init/lean/environment.lean +++ b/library/init/lean/environment.lean @@ -189,7 +189,7 @@ ext.toEnvExtension.modifyState env $ λ s, def forceStateAux {α σ : Type} (ext : PersistentEnvExtension α σ) (s : PersistentEnvExtensionState α σ) : σ := match s.state with | some d := d -| none := s.entries.foldl (ext.addEntryFn false) s.importedState.get +| none := s.entries.foldr (λ a s, ext.addEntryFn false s a) s.importedState.get def forceState {α σ : Type} (ext : PersistentEnvExtension α σ) (env : Environment) : Environment := ext.toEnvExtension.modifyState env $ λ s, { state := some (ext.forceStateAux s), .. s } @@ -301,7 +301,7 @@ let entries : Array (Name × Array EnvExtensionEntry) := pExts.size.fold let entryList := (pExts.get i).getEntries env in let toArrayFn := (pExts.get i).toArrayFn in let extName := (pExts.get i).name in - result.push (extName, toArrayFn entryList)) + result.push (extName, toArrayFn entryList.reverse)) Array.empty, bytes ← serializeModifications (modListExtension.getState env), pure {