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

fix(library/compiler/emit_cpp): Lean namespace

Browse source
This commit is contained in:
Sebastian Ullrich 2019-03-21 19:39:54 +01:00 • committed by Leonardo de Moura
parent 20451918a6
commit 09c65008f6
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/compiler/emit_cpp.cpp
View file

@ -1187,7 +1187,7 @@ void emit_cpp(std::ostream & out, environment const & env, module_name const & m
void initialize_emit_cpp() {
g_cpp = new name("cpp");
g_lean = new name("lean");
g_lean = new name("Lean");
}
void finalize_emit_cpp() {