From 33036befc60e2031100c8fa79713106bf75070c0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 13 Nov 2015 15:25:55 -0800 Subject: [PATCH] fix(library/blast/intros): corner case --- src/library/blast/intros.cpp | 2 ++ 1 file changed, 2 insertions(+) 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))