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

fix(library/compiler/emit_cpp): bug at emitting exported function headers

Browse source
This commit is contained in:
Leonardo de Moura 2019-02-14 14:35:27 -08:00
parent 68e8aa8d1d
commit a8ac25e1ef
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/compiler/emit_cpp.cpp
View file

@ -52,12 +52,12 @@ static void open_namespaces(std::ostream & out, name const & n) {
open_namespaces_core(out, n.get_prefix());
}
/* If `n` has the attribute [cppname], and the "cppname" is hierarchical, then
/* If `n` has the attribute [export], and the "export" is hierarchical, then
we must put `n` code inside of a namespace. */
static void open_namespaces_for(std::ostream & out, environment const & env, name const & n) {
optional<name> c = get_export_name_for(env, n);
if (!c || c->is_atomic()) return;
open_namespaces(out, n);
open_namespaces(out, *c);
}
static void close_namespaces(std::ostream & out, name const & n) {