From 9b60e25ca4bef9cf5356a19968cfdb2e05ce472b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 6 Jun 2017 16:12:35 -0700
Subject: [PATCH] fix(library/init/meta/level): make level as meta

---
 library/init/meta/level.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/library/init/meta/level.lean b/library/init/meta/level.lean
index 8b3a4f0dfc..c67c5e9c8e 100644
--- a/library/init/meta/level.lean
+++ b/library/init/meta/level.lean
@@ -7,7 +7,7 @@ prelude
 import init.meta.name init.meta.format
 
 /- Reflect a C++ level object. The VM replaces it with the C++ implementation. -/
-inductive level
+meta inductive level
 | zero   : level
 | succ   : level → level
 | max    : level → level → level
@@ -15,7 +15,7 @@ inductive level
 | param  : name → level
 | mvar   : name → level
 
-instance : inhabited level :=
+meta instance : inhabited level :=
 ⟨level.zero⟩
 
 /- TODO(Leo): provide a definition in Lean. -/