From ed73dafa484033e9365b97e83d696e5086aee793 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 18 Jul 2016 20:20:54 -0400 Subject: [PATCH] chore(library/tactic/unfold_tactic): fix style --- src/library/tactic/unfold_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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);