From 1a663afda4ec8088d341a525d27718b47b180d5a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 23 May 2014 10:50:34 -0700
Subject: [PATCH] feat(library/module): add extra function for adding
 uncertified declarations when trust_lvl > LEAN_BELIEVER_TRUST_LEVEL

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/module.cpp | 9 +++++++--
 src/library/module.h   | 5 +++++
 2 files changed, 12 insertions(+), 2 deletions(-)

diff --git a/src/library/module.cpp b/src/library/module.cpp
index 729b85593..e4c6be9e0 100644
--- a/src/library/module.cpp
+++ b/src/library/module.cpp
@@ -129,8 +129,13 @@ static register_module_object_reader_fn g_reg_decl_reader(g_decl, declaration_re
 
 environment add(environment const & env, certified_declaration const & d) {
     environment new_env = env.add(d);
-    new_env = add(new_env, g_decl, [=](serializer & s) { s << d.get_declaration(); });
-    return new_env;
+    declaration _d = d.get_declaration();
+    return add(new_env, g_decl, [=](serializer & s) { s << _d; });
+}
+
+environment add(environment const & env, declaration const & d) {
+    environment new_env = env.add(d);
+    return add(new_env, g_decl, [=](serializer & s) { s << d; });
 }
 
 struct import_modules_fn {
diff --git a/src/library/module.h b/src/library/module.h
index f61d8b29a..0ee5ae25a 100644
--- a/src/library/module.h
+++ b/src/library/module.h
@@ -70,4 +70,9 @@ environment add(environment const & env, std::string const & k, std::function<vo
 
 /** \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.
+    This method throws an exception if the trust_level <= LEAN_BELIEVER_TRUST_LEVEL
+*/
+environment add(environment const & env, declaration const & d);
 }