From 09c000fcb85f7368891c1a8a1dfdcd7eea05d000 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 31 Jul 2016 19:54:04 -0700
Subject: [PATCH] chore(frontends/lean/elaborator): remove unnecessary field

---
 src/frontends/lean/elaborator.cpp | 10 +++++-----
 src/frontends/lean/elaborator.h   |  9 ++++-----
 src/frontends/lean/parser.cpp     |  2 +-
 3 files changed, 10 insertions(+), 11 deletions(-)

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index eb66bf6cf6..c274e09e46 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -43,9 +43,9 @@ static type_context_cache & get_elab_tc_cache_for(environment const & env, optio
 #define trace_elab_detail(CODE) lean_trace("elaborator_detail", scope_trace_env _scope(m_env, m_ctx); CODE)
 #define trace_elab_debug(CODE) lean_trace("elaborator_debug", scope_trace_env _scope(m_env, m_ctx); CODE)
 
-elaborator::elaborator(environment const & env, options const & opts, local_level_decls const & lls,
-                       metavar_context const & mctx, local_context const & lctx, bool check_unassigend):
-    m_env(env), m_opts(opts), m_local_level_decls(lls),
+elaborator::elaborator(environment const & env, options const & opts, metavar_context const & mctx,
+                       local_context const & lctx, bool check_unassigend):
+    m_env(env), m_opts(opts),
     m_ctx(mctx, lctx, get_elab_tc_cache_for(env, opts), transparency_mode::Semireducible) {
     m_next_param_idx   = 1;
     m_check_unassigend = check_unassigend;
@@ -1439,9 +1439,9 @@ std::tuple<expr, level_param_names> elaborator::operator()(expr const & e) {
     return std::make_tuple(r, ls);
 }
 
-std::tuple<expr, level_param_names> elaborate(environment const & env, options const & opts, local_level_decls const & lls,
+std::tuple<expr, level_param_names> elaborate(environment const & env, options const & opts,
                                               metavar_context & mctx, local_context const & lctx, expr const & e, bool check_unassigend) {
-    elaborator elab(env, opts, lls, mctx, lctx, check_unassigend);
+    elaborator elab(env, opts, mctx, lctx, check_unassigend);
     auto r = elab(e);
     mctx = elab.mctx();
     return r;
diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h
index b623ab30b0..2fcad90211 100644
--- a/src/frontends/lean/elaborator.h
+++ b/src/frontends/lean/elaborator.h
@@ -27,7 +27,6 @@ class elaborator {
     };
     environment       m_env;
     options           m_opts;
-    local_level_decls m_local_level_decls;
     type_context      m_ctx;
 
     list<level>       m_uvar_stack;
@@ -204,14 +203,14 @@ class elaborator {
     void unassigned_uvars_to_params();
 
 public:
-    elaborator(environment const & env, options const & opts, local_level_decls const & lls,
-               metavar_context const & mctx, local_context const & lctx, bool check_unassigend);
+    elaborator(environment const & env, options const & opts, metavar_context const & mctx, local_context const & lctx,
+               bool check_unassigend);
     metavar_context const & mctx() const { return m_ctx.mctx(); }
     std::tuple<expr, level_param_names> operator()(expr const & e);
 };
 
-std::tuple<expr, level_param_names> elaborate(environment const & env, options const & opts, local_level_decls const & lls,
-                                              metavar_context & mctx, local_context const & lctx, expr const & e, bool check_unassigend);
+std::tuple<expr, level_param_names> elaborate(environment const & env, options const & opts, metavar_context & mctx, local_context const & lctx,
+                                              expr const & e, bool check_unassigend);
 
 void initialize_elaborator();
 void finalize_elaborator();
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 73ec2b077a..0c6c7b2a9f 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -914,7 +914,7 @@ elaborator_context parser::mk_elaborator_context(environment const & env, local_
 }
 
 std::tuple<expr, level_param_names> parser::elaborate(metavar_context & mctx, expr const & e, bool check_unassigned) {
-    return ::lean::elaborate(m_env, get_options(), m_local_level_decls, mctx, local_context(), e, check_unassigned);
+    return ::lean::elaborate(m_env, get_options(), mctx, local_context(), e, check_unassigned);
 }
 
 std::tuple<expr, level_param_names> parser::elaborate(expr const & e) {