From 9398b887cc7c7cc705f0e8552bd21b63817e9664 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 10 Feb 2015 18:34:45 -0800 Subject: [PATCH] fix(library/abbreviation): missing condition --- src/library/abbreviation.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/abbreviation.cpp b/src/library/abbreviation.cpp index abbae5ca8..22652804c 100644 --- a/src/library/abbreviation.cpp +++ b/src/library/abbreviation.cpp @@ -109,7 +109,7 @@ expr expand_abbreviations(environment const & env, expr const & e) { return e; abbrev_state const & s = abbrev_ext::get_state(env); 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))); else return none_expr();