diff --git a/src/library/module.cpp b/src/library/module.cpp
index fa585fed4..7eb1e3c98 100644
--- a/src/library/module.cpp
+++ b/src/library/module.cpp
@@ -38,6 +38,7 @@ typedef pair<std::string, std::function<void(serializer &)>> writer;
 struct module_ext : public environment_extension {
     list<module_name> m_direct_imports;
     list<writer>      m_writers;
+    name_set          m_module_defs;
 };
 
 struct module_ext_reg {
@@ -140,17 +141,34 @@ environment add_universe(environment const & env, name const & l) {
     return add(new_env, g_glvl_key, [=](serializer & s) { s << l; });
 }
 
+environment update_module_defs(environment const & env, declaration const & d) {
+    if (d.is_definition() && !d.is_theorem()) {
+        module_ext ext = get_extension(env);
+        ext.m_module_defs.insert(d.get_name());
+        return update(env, ext);
+    } else {
+        return env;
+    }
+}
+
 environment add(environment const & env, certified_declaration const & d) {
     environment new_env = env.add(d);
     declaration _d = d.get_declaration();
+    new_env = update_module_defs(new_env, _d);
     return add(new_env, g_decl_key, [=](serializer & s) { s << _d; });
 }
 
 environment add(environment const & env, declaration const & d) {
     environment new_env = env.add(d);
+    new_env = update_module_defs(new_env, d);
     return add(new_env, g_decl_key, [=](serializer & s) { s << d; });
 }
 
+bool is_definition(environment const & env, name const & n) {
+    module_ext const & ext = get_extension(env);
+    return ext.m_module_defs.contains(n);
+}
+
 static std::string g_inductive("ind");
 
 environment add_inductive(environment                  env,
diff --git a/src/library/module.h b/src/library/module.h
index fff16a638..9fc1c65df 100644
--- a/src/library/module.h
+++ b/src/library/module.h
@@ -31,22 +31,19 @@ public:
     optional<unsigned> const & get_k() const { return m_relative; }
 };
 
-/**
-   \brief Return an environment based on \c env, where all modules in \c modules are imported.
-   Modules included directly or indirectly by them are also imported.
-   The environment \c env is usually an empty environment.
+/** \brief Return an environment based on \c env, where all modules in \c modules are imported.
+    Modules included directly or indirectly by them are also imported.
+    The environment \c env is usually an empty environment.
 
-   If \c keep_proofs is false, then the proof of the imported theorems is discarded after being
-   checked. The idea is to save memory.
+    If \c keep_proofs is false, then the proof of the imported theorems is discarded after being
+    checked. The idea is to save memory.
 */
 environment import_modules(environment const & env, std::string const & base, unsigned num_modules, module_name const * modules,
                            unsigned num_threads, bool keep_proofs, io_state const & ios);
 environment import_module(environment const & env, std::string const & base, module_name const & module,
                           unsigned num_threads, bool keep_proofs, io_state const & ios);
 
-/**
-   \brief Store/Export module using \c env to the output stream \c out.
-*/
+/** \brief Store/Export module using \c env to the output stream \c out. */
 void export_module(std::ostream & out, environment const & env);
 
 /** \brief An asynchronous update. It goes into a task queue, and can be executed by a different execution thread. */
@@ -59,9 +56,8 @@ typedef std::function<void(shared_environment & env)> asynch_update_fn;
 */
 typedef std::function<environment(environment const & env, io_state const & ios)> delayed_update_fn;
 
-/**
-   \brief A reader for importing data from a stream using deserializer \c d.
-   There are three ways to update the environment being constructed.
+/** \brief A reader for importing data from a stream using deserializer \c d.
+    There are three ways to update the environment being constructed.
      1- Direct update it using \c senv.
      2- Asynchronous update using add_asynch_update.
      3- Delayed update using add_delayed_update.
@@ -70,9 +66,8 @@ typedef void (*module_object_reader)(deserializer & d, module_idx midx, shared_e
                                      std::function<void(asynch_update_fn const &)> & add_asynch_update,
                                      std::function<void(delayed_update_fn const &)> & add_delayed_update);
 
-/**
-   \brief Register a module object reader. The key \c k is used to identify the class of objects
-   that can be read by the given reader.
+/** \brief Register a module object reader. The key \c k is used to identify the class of objects
+    that can be read by the given reader.
 */
 void register_module_object_reader(std::string const & k, module_object_reader r);
 
@@ -84,8 +79,7 @@ struct register_module_object_reader_fn {
 };
 
 namespace module {
-/**
-    \brief Add a function that should be invoked when the environment is exported.
+/** \brief Add a function that should be invoked when the environment is exported.
     The key \c k identifies which module_object_reader should be used to deserialize the object
     when the module is imported.
 
@@ -98,12 +92,14 @@ environment add_universe(environment const & env, name const & l);
 
 /** \brief Add the given declaration to the environment, and mark it to be exported. */
 environment add(environment const & env, certified_declaration const & d);
-/**
-    \brief Add the given declaration to the environment, and mark it to be exported.
+/** \brief Add the given declaration to the environment, and mark it to be exported.
     This method throws an exception if the trust_level <= LEAN_BELIEVER_TRUST_LEVEL
 */
 environment add(environment const & env, declaration const & d);
 
+/** \brief Return true iff \c n is a definition added to the current module using #module::add */
+bool is_definition(environment const & env, name const & n);
+
 /** \brief Add the given inductive declaration to the environment, and mark it to be exported. */
 environment add_inductive(environment                  env,
                           level_param_names const &    level_params,