max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/private): make sure the private prefix is an internal name

Browse source
This commit is contained in:
Leonardo de Moura 2017-01-06 11:48:05 -08:00
parent 13a11b4374
commit d5da18299b
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/private.cpp
View file

@ -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();
}