michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontends/lean/elaborator): potential memory access violation

Browse source 
Before this commit, the modified method would crash if caching in the
whnf procedure was disabled.
This commit is contained in:
Leonardo de Moura 2015-03-10 10:12:40 -07:00
parent 1c55e2f389
commit 71ce207080
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

@ -434,7 +434,7 @@ pair<expr, expr> elaborator::ensure_fun(expr f, constraint_seq & cs) {
bool elaborator::has_coercions_from(expr const & a_type) {
try {
expr const & a_cls = get_app_fn(whnf(a_type).first);
expr a_cls = get_app_fn(whnf(a_type).first);
return is_constant(a_cls) && ::lean::has_coercions_from(env(), const_name(a_cls));
} catch (exception&) {
return false;