diff --git a/src/library/blast/intros.cpp b/src/library/blast/intros.cpp index 1935c059ee..d8793a43c5 100644 --- a/src/library/blast/intros.cpp +++ b/src/library/blast/intros.cpp @@ -24,6 +24,8 @@ struct intros_proof_step_cell : public proof_step_cell { }; bool intros_action(unsigned max) { + if (max == 0) + return true; state & s = curr_state(); expr target = whnf(s.get_target()); if (!is_pi(target))