From d5da18299bf9f67f9c7503d6d979ee6260181852 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 6 Jan 2017 11:48:05 -0800 Subject: [PATCH] feat(library/private): make sure the `private` prefix is an internal name --- src/library/private.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/private.cpp b/src/library/private.cpp index 1733547772..4a19d16399 100644 --- a/src/library/private.cpp +++ b/src/library/private.cpp @@ -93,7 +93,7 @@ bool is_private(environment const & env, name const & n) { void initialize_private() { g_ext = new private_ext_reg(); - g_private = new name("private"); + g_private = new name("_private"); private_modification::init(); }