From 6a079fdd2d6e8d135b9006d05053425f69c2dd79 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 7 Aug 2015 18:38:08 +0100 Subject: [PATCH] fix(library/tactic/exact_tactic): fixes #779 --- src/library/tactic/exact_tactic.cpp | 2 +- tests/lean/779.hlean | 4 ++++ tests/lean/779.hlean.expected.out | 2 ++ 3 files changed, 7 insertions(+), 1 deletion(-) create mode 100644 tests/lean/779.hlean create mode 100644 tests/lean/779.hlean.expected.out 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 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)