From 6eb377033b252f8dca594f03ab08cfbf83f69f9e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 26 May 2016 11:19:52 -0700
Subject: [PATCH] chore(library/system/IO): suppress unnecessary universe

---
 library/system/IO.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/system/IO.lean b/library/system/IO.lean
index 42a9020a21..8ce8090adb 100644
--- a/library/system/IO.lean
+++ b/library/system/IO.lean
@@ -3,7 +3,7 @@ Copyright (c) 2016 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Luke Nelson, Jared Roesch and Leonardo de Moura
 -/
-constant IO : Type → Type
+constant IO.{l} : Type.{l} → Type.{l}
 constant functorIO : functor IO
 constant monadIO : monad IO