From bd9df3b08fb731859d1e05625bcee0de23d7dae0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 6 Dec 2013 16:03:06 -0800
Subject: [PATCH] fix(library/tactic/goal): null hypothesis being added by
 to_goal

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

diff --git a/src/library/tactic/goal.cpp b/src/library/tactic/goal.cpp
index 40fedea8f..78154fd56 100644
--- a/src/library/tactic/goal.cpp
+++ b/src/library/tactic/goal.cpp
@@ -138,10 +138,10 @@ std::pair<goal, goal_proof_fn> to_goal(environment const & env, context const &
         expr b = replacer(e.get_body());
         replacer.clear();
         if (b && (!d || !inferer.is_proposition(d))) {
-            hypotheses.emplace_back(n, expr());
             bodies.push_back(b);
             consts.push_back(expr());
         } else {
+            lean_assert(d);
             hypotheses.emplace_back(n, d);
             bodies.push_back(expr());
             consts.push_back(mk_constant(n, d));