fix(library/scoped_ext): assertion

This commit is contained in:
Leonardo de Moura 2015-12-05 11:36:52 -08:00
parent 9736b8d79c
commit 07419617b0

View file

@ -309,7 +309,7 @@ public:
return update(env, get(env)._add_entry(env, ios, e));
}
} else {
lean_assert(!persistent);
lean_assert(persistent);
// add entry in a namespace that is not the current one
env = module::add(env, get_serialization_key(), [=](environment const &, serializer & s) {
s << n;