diff --git a/src/library/tactic/unfold_tactic.cpp b/src/library/tactic/unfold_tactic.cpp index f9a2cb1f40..8ac7ebd7c9 100644 --- a/src/library/tactic/unfold_tactic.cpp +++ b/src/library/tactic/unfold_tactic.cpp @@ -335,7 +335,7 @@ class unfold_rec_fn : public replace_visitor_aux { expr const new_head = get_app_fn(new_e); // TODO(Leo): create an option for the following conditions? if (is_constant(new_head) && inductive::is_elim_rule(m_env, const_name(new_head))) { - //head is a recursor... so the unfold is probably not generating a nice result... + // head is a recursor... so the unfold is probably not generating a nice result... throw fold_failed(); } return fold_rec_fn(m_ctx, fn, args, k, rec_name, indices_pos, main_pos, rec_arg_pos)(new_e);