From fe020b49c12f405f0a7d8323a545861009d1a828 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 4 Dec 2015 07:52:28 -0800 Subject: [PATCH] chore(library/scoped_ext): add comment --- src/library/scoped_ext.h | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/library/scoped_ext.h b/src/library/scoped_ext.h index 8558377b3..86c96f6e8 100644 --- a/src/library/scoped_ext.h +++ b/src/library/scoped_ext.h @@ -55,6 +55,14 @@ bool is_metaclass(name const & n); environment add_namespace(environment const & env, name const & ns); name const & get_namespace(environment const & env); +/** \brief Return the current stack of namespaces. + Example: at + namespace foo + namespace bla + namespace boo + - It returns [foo.bla.boo, foo.bla, foo] + + \remark This is *not* the set of opened namespaces. */ list const & get_namespaces(environment const & env); bool in_section(environment const & env);