From 20f31c85bf7140820c7e15c768fe0aa1b68d8a2e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 12 Sep 2018 20:36:32 -0700
Subject: [PATCH] chore(kernel/type_checker): we don't use the kernel type
 checker for elaboration anymore

---
 src/kernel/type_checker.h | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h
index bc76edd696..6c77909389 100644
--- a/src/kernel/type_checker.h
+++ b/src/kernel/type_checker.h
@@ -23,11 +23,7 @@ namespace lean {
 class type_checker {
 public:
     class context {
-        /* In the cache, we must take into account binder information.
-           Examples:
-           The type of (lambda x : A, t)   is (Pi x : A, typeof(t))
-           The type of (lambda {x : A}, t) is (Pi {x : A}, typeof(t)) */
-        typedef expr_bi_map<expr> infer_cache;
+        typedef expr_map<expr> infer_cache;
         typedef std::unordered_set<expr_pair, expr_pair_hash, expr_pair_eq> expr_pair_set;
         environment               m_env;
         name_generator            m_ngen;