From bd0f209659c9b814fc37c75e1c9ff0ebfe4fd318 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 5 Mar 2015 10:46:41 -0800 Subject: [PATCH] feat(library/tactic/exact_tactic): do not force 'exact' tactic expression to be fully elaborated (i.e., metavariable free) --- src/library/tactic/exact_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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);