diff --git a/src/library/tactic/exact_tactic.cpp b/src/library/tactic/exact_tactic.cpp
index 195af7c9e..0b5c91f69 100644
--- a/src/library/tactic/exact_tactic.cpp
+++ b/src/library/tactic/exact_tactic.cpp
@@ -34,7 +34,7 @@ tactic exact_tactic(elaborate_fn const & elab, expr const & e, bool enforce_type
                 return none_proof_state();
             }
             expr t                 = head(gs).get_type();
-            bool report_unassigned = !allow_metavars && enforce_type_during_elaboration;
+            bool report_unassigned = !allow_metavars && enforce_type_during_elaboration && s.report_failure();
             optional<expr> new_e;
             try {
                 new_e = elaborate_with_respect_to(env, ios, elab, new_s, e, some_expr(t),
diff --git a/tests/lean/779.hlean b/tests/lean/779.hlean
new file mode 100644
index 000000000..204cc370a
--- /dev/null
+++ b/tests/lean/779.hlean
@@ -0,0 +1,4 @@
+definition foo (x : empty) : empty :=
+by try exact _;contradiction
+
+print foo
diff --git a/tests/lean/779.hlean.expected.out b/tests/lean/779.hlean.expected.out
new file mode 100644
index 000000000..c169894a5
--- /dev/null
+++ b/tests/lean/779.hlean.expected.out
@@ -0,0 +1,2 @@
+definition foo : empty → empty :=
+empty.rec (λ (e : empty), empty)