From a8ba50531b681fe36ad801a0c24a7fb9ce1c8426 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 8 Sep 2013 20:38:11 -0700
Subject: [PATCH] Fix typo

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

diff --git a/src/library/reduce.cpp b/src/library/reduce.cpp
index 28ab44a25..52f5d3602 100644
--- a/src/library/reduce.cpp
+++ b/src/library/reduce.cpp
@@ -74,8 +74,7 @@ expr head_reduce(expr const & t, environment const & e, context const & c, name_
             if (obj && obj.is_definition() && !obj.is_opaque())
                 return obj.get_value();
         }
-    } else {
-        return t;
     }
+    return t;
 }
 }