fix(kernel/level): add missing LEAN_THREAD_LOCAL directive
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
a8a6bb1b7f
commit
d4922daedf
1 changed files with 2 additions and 2 deletions
|
@ -239,12 +239,12 @@ level mk_global_univ(name const & n) { return level(new level_param_core(level_k
|
||||||
level mk_meta_univ(name const & n) { return level(new level_param_core(level_kind::Meta, n)); }
|
level mk_meta_univ(name const & n) { return level(new level_param_core(level_kind::Meta, n)); }
|
||||||
|
|
||||||
level const & mk_level_zero() {
|
level const & mk_level_zero() {
|
||||||
static level g_zero(new level_cell(level_kind::Zero, 7u));
|
static LEAN_THREAD_LOCAL level g_zero(new level_cell(level_kind::Zero, 7u));
|
||||||
return g_zero;
|
return g_zero;
|
||||||
}
|
}
|
||||||
|
|
||||||
level const & mk_level_one() {
|
level const & mk_level_one() {
|
||||||
static level g_one(mk_succ(mk_level_zero()));
|
static LEAN_THREAD_LOCAL level g_one(mk_succ(mk_level_zero()));
|
||||||
return g_one;
|
return g_one;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue