From 437f44684449a8fd316de42cc0bc783271dfe4f1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 19 Mar 2019 11:24:23 -0700
Subject: [PATCH] chore(library/type_context): error instead of assertion
 violation

---
 src/library/type_context.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 5d8a442f56..09ece1fab4 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -633,8 +633,8 @@ optional<expr> type_context_old::reduce_projection(expr const & e) {
 }
 
 optional<expr> type_context_old::reduce_proj(expr const & /* e */) {
-    // TODO(Leo):
-    lean_unreachable();
+    // TODO(Leo)
+    throw exception("projection reduction is only implemented in the kernel.");
 }
 
 optional<expr> type_context_old::reduce_aux_recursor(expr const & e) {