From 582117da96c28e558ec6a39edb65f16fe3c9baeb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 1 Aug 2016 16:35:42 -0700 Subject: [PATCH] fix(frontends/lean/elaborator): elaborator must take into account binder information when caching inferred types --- src/frontends/lean/elaborator.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index db8de441fa..aed8f474c1 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -34,7 +34,7 @@ Author: Leonardo de Moura #include "frontends/lean/elaborator.h" namespace lean { -MK_THREAD_LOCAL_GET_DEF(type_context_cache_helper, get_tch); +MK_THREAD_LOCAL_GET(type_context_cache_helper, get_tch, true /* use binder information at infer_cache */); static type_context_cache & get_elab_tc_cache_for(environment const & env, options const & o) { return get_tch().get_cache_for(env, o);