From db39458c30c76b552cbe60aa17078437cf681b22 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 7 May 2014 16:22:08 -0700 Subject: [PATCH] fix(kernel/level): predicate is_param_core Signed-off-by: Leonardo de Moura --- src/kernel/level.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp index df70464ef3..0d1e62e9e7 100644 --- a/src/kernel/level.cpp +++ b/src/kernel/level.cpp @@ -101,7 +101,7 @@ struct level_param_core : public level_cell { } }; -bool is_param_core(level const & l) { return is_param(l) || is_meta(l); } +bool is_param_core(level const & l) { return is_param(l) || is_global(l) || is_meta(l); } static level_param_core const & to_param_core(level const & l) { lean_assert(is_param_core(l));