diff --git a/src/library/compiler/preprocess.cpp b/src/library/compiler/preprocess.cpp
index 8ca12c3520..791328266f 100644
--- a/src/library/compiler/preprocess.cpp
+++ b/src/library/compiler/preprocess.cpp
@@ -252,9 +252,10 @@ class preprocess_fn {
                                               v4, reducibility_hints::mk_opaque(), true);
         /* IMPORTANT: We do not need to save the auxiliary declaration in the environment.
            This is just a temporary hack.
-           We should store this information in a different place. Otherwise, we will have
-           to pay the price of type checking this auxiliary declaration. */
-        m_env = module::add(m_env, simp_decl);
+           We should store this information in a different place. In the meantime,
+           I just invoke `module::add` with `check = false`. This is a temporary
+           solution since we will not have this parameter in the final version. */
+        m_env = module::add(m_env, simp_decl, false);
     }
 
     name get_real_name(name const & n) {
diff --git a/src/library/module.cpp b/src/library/module.cpp
index 4e3bed564b..d904e879eb 100644
--- a/src/library/module.cpp
+++ b/src/library/module.cpp
@@ -191,8 +191,8 @@ environment add_and_perform(environment const & env, std::shared_ptr<modificatio
     return update(new_env, ext);
 }
 
-environment add(environment const & env, declaration const & d) {
-    environment new_env = env.add(d);
+environment add(environment const & env, declaration const & d, bool check) {
+    environment new_env = env.add(d, check);
     if (d.is_definition()) {
         definition_val const & v = d.to_definition_val();
         if (!check_computable(new_env, v.get_name()))
diff --git a/src/library/module.h b/src/library/module.h
index b228510aa2..cf9b0d8cbc 100644
--- a/src/library/module.h
+++ b/src/library/module.h
@@ -99,7 +99,7 @@ environment add(environment const & env, std::shared_ptr<modification const> con
 environment add_and_perform(environment const & env, std::shared_ptr<modification const> const & modif);
 
 /** \brief Add the given declaration to the environment, and mark it to be exported. */
-environment add(environment const & env, declaration const & d);
+environment add(environment const & env, declaration const & d, bool check = true);
 }
 void initialize_module();
 void finalize_module();