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 reduce(expr const & e, list const & to_unfold, optional const & occs, bool force_unfold) { - lean_assert(is_nil(to_unfold) == !occs); constraint_seq cs; bool unfolded = !to_unfold; bool use_eta = true;