diff --git a/src/library/tactic/exact_tactic.cpp b/src/library/tactic/exact_tactic.cpp index 9767d827e..0760b526a 100644 --- a/src/library/tactic/exact_tactic.cpp +++ b/src/library/tactic/exact_tactic.cpp @@ -20,7 +20,7 @@ tactic exact_tactic(elaborate_fn const & elab, expr const & e) { return none_proof_state(); } expr t = head(gs).get_type(); - bool report_unassigned = true; + bool report_unassigned = false; if (auto new_e = elaborate_with_respect_to(env, ios, elab, new_s, e, some_expr(t), report_unassigned)) { goals const & gs = new_s.get_goals(); goal const & g = head(gs);