diff --git a/src/library/private.cpp b/src/library/private.cpp index 693a6d834..f6db2f0eb 100644 --- a/src/library/private.cpp +++ b/src/library/private.cpp @@ -10,6 +10,7 @@ Author: Leonardo de Moura #include "library/private.h" #include "library/module.h" #include "library/kernel_bindings.h" +#include "library/fingerprint.h" namespace lean { struct private_ext : public environment_extension { @@ -43,6 +44,9 @@ static environment preserve_private_data(environment const & env, name const & r pair add_private_name(environment const & env, name const & n, optional const & extra_hash) { private_ext ext = get_extension(env); unsigned h = hash(n.hash(), ext.m_counter); + uint64 f = get_fingerprint(env); + h = hash(h, static_cast(f >> 32)); + h = hash(h, static_cast(f)); if (extra_hash) h = hash(h, *extra_hash); name r = name(*g_private, h) + n; diff --git a/tests/lean/hott/648.hlean b/tests/lean/hott/648.hlean new file mode 100644 index 000000000..224304591 --- /dev/null +++ b/tests/lean/hott/648.hlean @@ -0,0 +1 @@ +import hit.colimit hit.pushout