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

fix(library/compiler/erase_irrelevant): erase_type

Browse source
This commit is contained in:
Leonardo de Moura 2018-02-19 07:55:43 -08:00
parent a7afedc5c3
commit dbfcc65c60
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/library/compiler/erase_irrelevant.cpp
View file

@ -93,7 +93,7 @@ class erase_irrelevant_fn : public compiler_step_visitor {
}
expr erase_type(expr const & e) {
if (closed(e))
if (closed(e) && !has_local(e))
return e; // keep closed types for runtime debugger
else
return *g_neutral_expr;