diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index c2c336189..485b8b696 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -167,4 +167,8 @@ environment environment::update(unsigned id, std::shared_ptr<environment_extensi
     (*new_exts)[id] = ext;
     return environment(m_header, m_id, m_definitions, m_global_levels, new_exts);
 }
+
+void environment::for_each(std::function<void(definition const & d)> const & f) const {
+    m_definitions.for_each([&](name const &, definition const & d) { return f(d); });
+}
 }
diff --git a/src/kernel/environment.h b/src/kernel/environment.h
index 42e7fe852..8d3c290fd 100644
--- a/src/kernel/environment.h
+++ b/src/kernel/environment.h
@@ -196,6 +196,9 @@ public:
         is not pointer equal to the result.
     */
     environment forget() const;
+
+    /** \brief Apply the function \c f to each definition */
+    void for_each(std::function<void(definition const & d)> const & f) const;
 };
 
 class name_generator;