max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(frontends/lean/elaborator): elaborator must take into account binder information when caching inferred types

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-01 16:35:42 -07:00
parent a50e13f538
commit 582117da96
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/elaborator.cpp
View file

@ -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);