diff --git a/src/util/name.h b/src/util/name.h index fe5c46004c..306eaa7858 100644 --- a/src/util/name.h +++ b/src/util/name.h @@ -14,7 +14,7 @@ Author: Leonardo de Moura #include "util/list.h" namespace lean { -constexpr char const * lean_name_separator = "::"; +constexpr char const * lean_name_separator = "."; enum class name_kind { ANONYMOUS, STRING, NUMERAL }; /** \brief Hierarchical names.