From 6a87239a5d34bd8cd39612f08089f39897a7e6c5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 21 May 2015 10:13:44 -0700
Subject: [PATCH] chore(kernel/justification): fix compilation warning

---
 src/kernel/justification.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/kernel/justification.cpp b/src/kernel/justification.cpp
index fd2e55993..8546d9396 100644
--- a/src/kernel/justification.cpp
+++ b/src/kernel/justification.cpp
@@ -315,6 +315,7 @@ format justification::pp_core(formatter const & fmt, pos_info_provider const * p
         format r2 = to_composite(it)->m_child[1].pp_core(fmt, p, s, set, false);
         return r1 + r2;
     }}
+    lean_unreachable();
 }
 
 format justification::pp(formatter const & fmt, pos_info_provider const * p, substitution const & s) const {