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

fix(library/abbreviation): missing condition

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-10 18:34:45 -08:00
parent bd304e1911
commit 9398b887cc
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/abbreviation.cpp
View file

@ -109,7 +109,7 @@ expr expand_abbreviations(environment const & env, expr const & e) {
return e; return e;
abbrev_state const & s = abbrev_ext::get_state(env); abbrev_state const & s = abbrev_ext::get_state(env);
return replace(e, [&](expr const & e, unsigned) { return replace(e, [&](expr const & e, unsigned) {
if (s.is_abbreviation(const_name(e))) if (is_constant(e) && s.is_abbreviation(const_name(e)))
return some_expr(instantiate_value_univ_params(env.get(const_name(e)), const_levels(e))); return some_expr(instantiate_value_univ_params(env.get(const_name(e)), const_levels(e)));
else else
return none_expr(); return none_expr();