From c2edc330ef5e5585ed182063ea909e36f75c3877 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 13 Jul 2015 19:19:12 -0400
Subject: [PATCH] fix(library/tactic/rewrite_tactic): remove incorrect
 assertion

---
 src/library/tactic/rewrite_tactic.cpp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp
index 92f5c79f2..05aa5ff44 100644
--- a/src/library/tactic/rewrite_tactic.cpp
+++ b/src/library/tactic/rewrite_tactic.cpp
@@ -629,7 +629,6 @@ class rewrite_fn {
     };
 
     optional<expr> reduce(expr const & e, list<name> const & to_unfold, optional<occurrence> const & occs, bool force_unfold) {
-        lean_assert(is_nil(to_unfold) == !occs);
         constraint_seq cs;
         bool unfolded = !to_unfold;
         bool use_eta  = true;