From d58b8a81022474c9eef300c0c2c16d52f7931a6e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 15 May 2014 10:46:04 -0700
Subject: [PATCH] refactor(kernel): move delayed_justification to
 justification.h

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/converter.h     | 9 ---------
 src/kernel/justification.h | 9 +++++++++
 2 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/src/kernel/converter.h b/src/kernel/converter.h
index d8ae68047..abd7e4e2a 100644
--- a/src/kernel/converter.h
+++ b/src/kernel/converter.h
@@ -8,15 +8,6 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 
 namespace lean {
-/** \brief Object to simulate delayed justification creation. */
-class delayed_justification {
-    optional<justification>        m_jst;
-    std::function<justification()> m_mk;
-public:
-    template<typename Mk> delayed_justification(Mk && mk):m_mk(mk) {}
-    justification get() { if (!m_jst) { m_jst = m_mk(); } return *m_jst; }
-};
-
 /** \brief Auxiliary exception used to sign that constraints cannot be created when \c m_cnstrs_enabled flag is false. */
 struct add_cnstr_exception {};
 
diff --git a/src/kernel/justification.h b/src/kernel/justification.h
index 66216245a..e95ef1ae5 100644
--- a/src/kernel/justification.h
+++ b/src/kernel/justification.h
@@ -140,4 +140,13 @@ bool depends_on(justification const & j, unsigned i);
 
 /** \brief Printer for debugging purposes */
 std::ostream & operator<<(std::ostream & out, justification const & j);
+
+/** \brief Object to simulate delayed justification creation. */
+class delayed_justification {
+    optional<justification>        m_jst;
+    std::function<justification()> m_mk;
+public:
+    template<typename Mk> delayed_justification(Mk && mk):m_mk(mk) {}
+    justification get() { if (!m_jst) { m_jst = m_mk(); } return *m_jst; }
+};
 }