From 4c275309302159fa783e308f1e3ad6666ce7c0cf Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 30 Aug 2013 17:07:45 -0700
Subject: [PATCH] Fix missing case in the elaborator

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/elaborator.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/library/elaborator.cpp b/src/library/elaborator.cpp
index 3be884437..a2a22946b 100644
--- a/src/library/elaborator.cpp
+++ b/src/library/elaborator.cpp
@@ -123,6 +123,8 @@ class elaborator::imp {
             return level();
         } else if (is_type(e)) {
             return ty_level(e);
+        } else if (e == Bool) {
+            return level();
         } else {
             expr r = head_reduce_mmv(e, m_env, m_available_defs);
             if (!is_eqp(r, e)) {