diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index a0554a2546..f60f39e9cb 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -245,18 +245,6 @@ expr elaborator::recoverable_error(optional<expr> const & expected_type, expr co
     return mk_sorry(expected_type, ref);
 }
 
-template <class Fn>
-expr elaborator::recover_expr_from_exception(optional<expr> const & expected_type, expr const & ref, Fn && fn) {
-    try {
-        return fn();
-    } catch (std::exception & ex) {
-        if (!try_report(ex, some_expr(ref))) {
-            throw;
-        } else {
-            return mk_sorry(expected_type, ref);
-        }
-    }
-}
 
 level elaborator::mk_univ_metavar() {
     return m_ctx.mk_univ_metavar_decl();
@@ -2372,7 +2360,7 @@ expr elaborator::visit_equations(expr const & e) {
     new_e = instantiate_mvars(new_e);
     ensure_no_unassigned_metavars(new_e);
     metavar_context mctx = m_ctx.mctx();
-    expr r = compile_equations(m_env, m_opts, mctx, m_ctx.lctx(), new_e);
+    expr r = compile_equations(m_env, m_opts, mctx, m_ctx.lctx(), new_e, *this);
     m_ctx.set_env(m_env);
     m_ctx.set_mctx(mctx);
     return r;
diff --git a/src/frontends/lean/elaborator.h b/src/frontends/lean/elaborator.h
index 823843311e..f4f51f11f6 100644
--- a/src/frontends/lean/elaborator.h
+++ b/src/frontends/lean/elaborator.h
@@ -157,6 +157,8 @@ private:
 
     bool has_synth_sorry(expr const & e) { return has_synth_sorry({e}); }
     bool has_synth_sorry(std::initializer_list<expr> && es);
+
+public:
     bool try_report(std::exception const & ex);
     bool try_report(std::exception const & ex, optional<expr> const & ref);
     void report_or_throw(elaborator_exception const & ex);
@@ -165,6 +167,7 @@ private:
     expr recoverable_error(optional<expr> const & expected_type, expr const & ref, elaborator_exception const & ex);
     template <class Fn> expr recover_expr_from_exception(optional<expr> const & expected_type, expr const & ref, Fn &&);
 
+private:
     expr ensure_type(expr const & e, expr const & ref);
     expr ensure_function(expr const & e, expr const & ref);
     optional<expr> ensure_has_type(expr const & e, expr const & e_type, expr const & type, expr const & ref);
@@ -343,6 +346,19 @@ public:
     bool has_errors() const { return m_has_errors; }
 };
 
+template <class Fn>
+expr elaborator::recover_expr_from_exception(optional<expr> const & expected_type, expr const & ref, Fn && fn) {
+    try {
+        return fn();
+    } catch (std::exception & ex) {
+        if (!try_report(ex, some_expr(ref))) {
+            throw;
+        } else {
+            return mk_sorry(expected_type, ref);
+        }
+    }
+}
+
 pair<expr, level_param_names> elaborate(environment & env, options const & opts, name const & decl_name,
                                         metavar_context & mctx, local_context const & lctx,
                                         expr const & e, bool check_unassigned, bool recover_from_errors);
diff --git a/src/library/equations_compiler/compiler.cpp b/src/library/equations_compiler/compiler.cpp
index 793daa3011..962fee5ce4 100644
--- a/src/library/equations_compiler/compiler.cpp
+++ b/src/library/equations_compiler/compiler.cpp
@@ -17,6 +17,7 @@ Author: Leonardo de Moura
 #include "library/equations_compiler/unbounded_rec.h"
 #include "library/equations_compiler/wf_rec.h"
 #include "library/equations_compiler/elim_match.h"
+#include "frontends/lean/elaborator.h"
 
 namespace lean {
 #define trace_compiler(Code) lean_trace("eqn_compiler", scope_trace_env _scope1(ctx.env(), ctx); Code)
@@ -29,7 +30,7 @@ static bool has_nested_rec(expr const & eqns) {
 
 static eqn_compiler_result compile_equations_core(environment & env, options const & opts,
                                    metavar_context & mctx, local_context const & lctx,
-                                   expr const & eqns) {
+                                   expr const & eqns, elaborator & elab) {
     type_context ctx(env, opts, mctx, lctx, transparency_mode::Semireducible);
     trace_compiler(tout() << "compiling\n" << eqns << "\n";);
     trace_compiler(tout() << "recursive:          " << is_recursive_eqns(ctx, eqns) << "\n";);
@@ -42,22 +43,22 @@ static eqn_compiler_result compile_equations_core(environment & env, options con
         if (is_wf_equations(eqns)) {
             throw exception("invalid use of 'using_well_founded', we do not need to use well founded recursion for meta definitions, since they can use unbounded recursion");
         }
-        return unbounded_rec(env, opts, mctx, lctx, eqns);
+        return unbounded_rec(env, opts, mctx, lctx, eqns, elab);
     }
 
     if (is_wf_equations(eqns)) {
-        return wf_rec(env, opts, mctx, lctx, eqns);
+        return wf_rec(env, opts, mctx, lctx, eqns, elab);
     }
 
     if (header.m_num_fns == 1) {
         if (!is_recursive_eqns(ctx, eqns)) {
-            return mk_nonrec(env, opts, mctx, lctx, eqns);
-        } else if (auto r = try_structural_rec(env, opts, mctx, lctx, eqns)) {
+            return mk_nonrec(env, opts, mctx, lctx, eqns, elab);
+        } else if (auto r = try_structural_rec(env, opts, mctx, lctx, eqns, elab)) {
             return *r;
         }
     }
 
-    return wf_rec(env, opts, mctx, lctx, eqns);
+    return wf_rec(env, opts, mctx, lctx, eqns, elab);
 }
 
 /** Auxiliary class for pulling nested recursive calls.
@@ -276,11 +277,11 @@ struct pull_nested_rec_fn : public replace_visitor {
         }
     }
 
-    eqn_compiler_result operator()(expr const & e) {
+    eqn_compiler_result operator()(expr const & e, elaborator & elab) {
         expr new_e             = visit(e);
         lean_assert(m_lctx_stack.size() == 1);
         local_context new_lctx = m_lctx_stack[0];
-        auto r                 = compile_equations_core(m_env, m_opts, m_mctx, new_lctx, new_e);
+        auto r                 = compile_equations_core(m_env, m_opts, m_mctx, new_lctx, new_e, elab);
         type_context ctx       = mk_type_context(new_lctx);
         r.m_fns = map(r.m_fns, [&] (expr const & fn) { return replace_locals(fn, m_new_locals, m_new_values); });
         m_mctx                 = ctx.mctx();
@@ -302,14 +303,14 @@ static expr remove_aux_main_name(expr const & e) {
 }
 
 expr compile_equations(environment & env, options const & opts, metavar_context & mctx, local_context const & lctx,
-                       expr const & _eqns) {
+                       expr const & _eqns, elaborator & elab) {
     expr eqns = _eqns;
     equations_header const & header = get_equations_header(eqns);
     eqn_compiler_result r;
     if (!header.m_is_meta && has_nested_rec(eqns)) {
-        r = pull_nested_rec_fn(env, opts, mctx, lctx)(eqns);
+        r = pull_nested_rec_fn(env, opts, mctx, lctx)(eqns, elab);
     } else {
-        r = compile_equations_core(env, opts, mctx, lctx, eqns);
+        r = compile_equations_core(env, opts, mctx, lctx, eqns, elab);
     }
 
     if (r.m_counter_examples) {
@@ -318,7 +319,7 @@ expr compile_equations(environment & env, options const & opts, metavar_context
         for (auto & ce : r.m_counter_examples) {
             fmt += line() + pp(remove_aux_main_name(ce));
         }
-        throw formatted_exception(_eqns, fmt);
+        elab.report_or_throw({_eqns, fmt});
     }
 
     buffer<expr> fns; to_buffer(r.m_fns, fns);
diff --git a/src/library/equations_compiler/compiler.h b/src/library/equations_compiler/compiler.h
index 3d25a0f285..e87094fea6 100644
--- a/src/library/equations_compiler/compiler.h
+++ b/src/library/equations_compiler/compiler.h
@@ -8,8 +8,9 @@ Author: Leonardo de Moura
 #include "library/metavar_context.h"
 #include "library/equations_compiler/equations.h"
 namespace lean {
+class elaborator;
 expr compile_equations(environment & env, options const & opts, metavar_context & mctx, local_context const & lctx,
-                       expr const & eqns);
+                       expr const & eqns, elaborator & elab);
 void initialize_compiler();
 void finalize_compiler();
 }
diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp
index b2f42eabe6..ba9cddc639 100644
--- a/src/library/equations_compiler/elim_match.cpp
+++ b/src/library/equations_compiler/elim_match.cpp
@@ -38,6 +38,7 @@ Author: Leonardo de Moura
 #include "library/equations_compiler/equations.h"
 #include "library/equations_compiler/util.h"
 #include "library/equations_compiler/elim_match.h"
+#include "frontends/lean/elaborator.h"
 
 #ifndef LEAN_DEFAULT_EQN_COMPILER_ITE
 #define LEAN_DEFAULT_EQN_COMPILER_ITE true
@@ -66,6 +67,7 @@ struct elim_match_fn {
     environment     m_env;
     options         m_opts;
     metavar_context m_mctx;
+    elaborator &    m_elab;
 
     expr            m_ref;
     unsigned        m_depth{0};
@@ -73,6 +75,8 @@ struct elim_match_fn {
     bool            m_aux_lemmas;
     unsigned        m_num_steps{0};
 
+    bool m_error_during_process = false;
+
     /* configuration options */
     bool            m_use_ite;
     unsigned        m_max_steps;
@@ -82,8 +86,8 @@ struct elim_match_fn {
     name_map<bool>  m_enum;
 
     elim_match_fn(environment const & env, options const & opts,
-                  metavar_context const & mctx):
-        m_env(env), m_opts(opts), m_mctx(mctx) {
+                  metavar_context const & mctx, elaborator & elab):
+        m_env(env), m_opts(opts), m_mctx(mctx), m_elab(elab) {
         m_use_ite   = get_eqn_compiler_ite(opts);
         m_max_steps = get_eqn_compiler_max_steps(opts);
     }
@@ -1237,41 +1241,43 @@ struct elim_match_fn {
         trace_match(tout() << "depth [" << m_depth << "]\n" << pp_problem(P) << "\n";);
         lean_assert(check_problem(P));
         m_num_steps++;
-        if (m_num_steps > m_max_steps) {
-            throw_error(sstream() << "equation compiler failed, maximum number of steps (" << m_max_steps << ") exceeded"
-                        << " (possible solution: use 'set_option eqn_compiler.max_steps <new-threshold>')"
-                        << " (use 'set_option trace.eqn_compiler.elim_match true' for additional details)");
-        }
-        if (P.m_var_stack) {
-            if (!P.m_equations) {
-                return process_no_equation(P);
-            } else if (!is_next_var(P)) {
-                return process_non_variable(P);
-            } else if (is_variable_transition(P)) {
-                return process_variable(P);
-            } else if (is_value_transition(P)) {
-                return process_value(P);
-            } else if (is_complete_transition(P)) {
-                return process_complete(P);
-            } else if (is_constructor_transition(P)) {
-                return process_constructor(P);
-            } else if (is_transport_transition(P)) {
-                return process_transport(P);
-            } else if (is_inaccessible_transition(P)) {
-                return process_inaccessible(P);
-            } else {
-                trace_match(tout() << "compilation failed at\n" << pp_problem(P) << "\n";);
-                if (!m_unsolved.empty()) {
-                    // report non-exhaustive match
-                    m_mctx.assign(P.m_goal, mk_sorry(m_mctx.get_metavar_decl(P.m_goal).get_type(), true));
-                    return list<lemma>();
-                }
-                throw_error("equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' "
-                            "for additional details)");
+        try {
+            if (m_num_steps > m_max_steps) {
+                throw_error(sstream() << "equation compiler failed, maximum number of steps (" << m_max_steps << ") exceeded"
+                            << " (possible solution: use 'set_option eqn_compiler.max_steps <new-threshold>')"
+                            << " (use 'set_option trace.eqn_compiler.elim_match true' for additional details)");
             }
-        } else {
-            return process_leaf(P);
+            if (P.m_var_stack) {
+                if (!P.m_equations) {
+                    return process_no_equation(P);
+                } else if (!is_next_var(P)) {
+                    return process_non_variable(P);
+                } else if (is_variable_transition(P)) {
+                    return process_variable(P);
+                } else if (is_value_transition(P)) {
+                    return process_value(P);
+                } else if (is_complete_transition(P)) {
+                    return process_complete(P);
+                } else if (is_constructor_transition(P)) {
+                    return process_constructor(P);
+                } else if (is_transport_transition(P)) {
+                    return process_transport(P);
+                } else if (is_inaccessible_transition(P)) {
+                    return process_inaccessible(P);
+                } else {
+                    trace_match(tout() << "compilation failed at\n" << pp_problem(P) << "\n";);
+                    throw_error("equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' "
+                                "for additional details)");
+                }
+            } else {
+                return process_leaf(P);
+            }
+        } catch (exception & ex) {
+            if (!m_elab.try_report(ex, some_expr(m_ref))) throw;
+            m_error_during_process = true;
+            m_mctx.assign(P.m_goal, mk_sorry(m_mctx.get_metavar_decl(P.m_goal).get_type(), true));
         }
+        return list<lemma>();
     }
 
     expr finalize_lemma(expr const & fn, lemma const & L) {
@@ -1313,12 +1319,14 @@ struct elim_match_fn {
                 expr ref = eqns_buffer[i];
                 while (is_lambda(ref)) ref = binding_body(ref);
                 if (j != i) {
-                    throw generic_exception(ref, sstream() << "equation compiler error, equation #" << (i+1)
+                    m_elab.report_or_throw(elaborator_exception(ref,
+                                  sstream() << "equation compiler error, equation #" << (i+1)
                                             << " has not been used in the compilation, note that the left-hand-side of equation #" << (j+1)
-                                            << " is a variable");
+                                            << " is a variable"));
                 } else {
-                    throw generic_exception(ref, sstream() << "equation compiler error, equation #" << (i+1)
-                                            << " has not been used in the compilation (possible solution: delete equation)");
+                    m_elab.report_or_throw(elaborator_exception(ref,
+                                  sstream() << "equation compiler error, equation #" << (i+1)
+                                            << " has not been used in the compilation (possible solution: delete equation)"));
                 }
             }
         }
@@ -1354,7 +1362,8 @@ struct elim_match_fn {
         lean_assert(check_problem(P));
         list<lemma> pre_Ls       = process(P);
         auto counter_examples    = get_counter_examples();
-        if (!counter_examples) check_no_unused_eqns(eqns);
+        if (!counter_examples && !m_error_during_process)
+            check_no_unused_eqns(eqns);
         fn                       = m_mctx.instantiate_mvars(fn);
         trace_match_debug(tout() << "code:\n" << fn << "\n";);
         list<expr> Ls            = finalize_lemmas(fn, pre_Ls);
@@ -1363,8 +1372,8 @@ struct elim_match_fn {
 };
 
 elim_match_result elim_match(environment & env, options const & opts, metavar_context & mctx,
-                             local_context const & lctx, expr const & eqns) {
-    elim_match_fn elim(env, opts, mctx);
+                             local_context const & lctx, expr const & eqns, elaborator & elab) {
+    elim_match_fn elim(env, opts, mctx, elab);
     auto r = elim(lctx, eqns);
     env = elim.m_env;
     return r;
@@ -1378,9 +1387,9 @@ static expr get_fn_type_from_eqns(expr const & eqns) {
 }
 
 eqn_compiler_result mk_nonrec(environment & env, options const & opts, metavar_context & mctx,
-               local_context const & lctx, expr const & eqns) {
+               local_context const & lctx, expr const & eqns, elaborator & elab) {
     equations_header header = get_equations_header(eqns);
-    auto R = elim_match(env, opts, mctx, lctx, eqns);
+    auto R = elim_match(env, opts, mctx, lctx, eqns, elab);
     if (header.m_is_meta || header.m_is_lemma) {
         /* Do not generate auxiliary equation or equational lemmas */
         auto fn = mk_constant(head(header.m_fn_names));
diff --git a/src/library/equations_compiler/elim_match.h b/src/library/equations_compiler/elim_match.h
index e177693ef4..625e51e6c5 100644
--- a/src/library/equations_compiler/elim_match.h
+++ b/src/library/equations_compiler/elim_match.h
@@ -8,14 +8,17 @@ Author: Leonardo de Moura
 #include "library/type_context.h"
 #include "library/equations_compiler/util.h"
 namespace lean {
+class elaborator;
 struct elim_match_result {
     expr       m_fn;
     list<expr> m_lemmas;
     list<list<expr>> m_counter_examples;
 };
-elim_match_result elim_match(environment & env, options const & opts, metavar_context & mctx, local_context const & lctx, expr const & eqns);
+elim_match_result elim_match(environment & env, options const & opts, metavar_context & mctx,
+                local_context const & lctx, expr const & eqns, elaborator & elab);
 eqn_compiler_result mk_nonrec(environment & env, options const & opts, metavar_context & mctx,
-               local_context const & lctx, expr const & eqns);
+               local_context const & lctx, expr const & eqns,
+               elaborator & elab);
 void initialize_elim_match();
 void finalize_elim_match();
 }
diff --git a/src/library/equations_compiler/structural_rec.cpp b/src/library/equations_compiler/structural_rec.cpp
index 4760b3271c..80e996f545 100644
--- a/src/library/equations_compiler/structural_rec.cpp
+++ b/src/library/equations_compiler/structural_rec.cpp
@@ -957,12 +957,12 @@ struct structural_rec_fn {
         }
     }
 
-    optional<eqn_compiler_result> operator()(expr const & eqns) {
+    optional<eqn_compiler_result> operator()(expr const & eqns, elaborator & elab) {
         m_ref    = eqns;
         m_header = get_equations_header(eqns);
         auto new_eqns = elim_recursion(eqns);
         if (!new_eqns) return {};
-        elim_match_result R = elim_match(m_env, m_opts, m_mctx, m_lctx, *new_eqns);
+        elim_match_result R = elim_match(m_env, m_opts, m_mctx, m_lctx, *new_eqns, elab);
         expr fn = mk_function(R.m_fn);
         if (m_header.m_aux_lemmas) {
             lean_assert(!m_header.m_is_meta);
@@ -977,9 +977,9 @@ struct structural_rec_fn {
 };
 
 optional<eqn_compiler_result> try_structural_rec(environment & env, options const & opts, metavar_context & mctx,
-                                  local_context const & lctx, expr const & eqns) {
+                                  local_context const & lctx, expr const & eqns, elaborator & elab) {
     structural_rec_fn F(env, opts, mctx, lctx);
-    if (auto r = F(eqns)) {
+    if (auto r = F(eqns, elab)) {
         env  = F.env();
         mctx = F.mctx();
         return r;
diff --git a/src/library/equations_compiler/structural_rec.h b/src/library/equations_compiler/structural_rec.h
index a6bab91822..a0cb530848 100644
--- a/src/library/equations_compiler/structural_rec.h
+++ b/src/library/equations_compiler/structural_rec.h
@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "library/type_context.h"
 #include "library/equations_compiler/util.h"
 namespace lean {
+class elaborator;
 /** \brief Try to eliminate "recursive calls" in the equations \c eqns by using brec_on's below.
     If successful, elim_match is used to compile pattern matching.
 
@@ -17,7 +18,7 @@ namespace lean {
        construction, where every recursive call is structurally smaller. */
 optional<eqn_compiler_result> try_structural_rec(environment & env, options const & opts,
                                   metavar_context & mctx, local_context const & lctx,
-                                  expr const & eqns);
+                                  expr const & eqns, elaborator & elab);
 
 void initialize_structural_rec();
 void finalize_structural_rec();
diff --git a/src/library/equations_compiler/unbounded_rec.cpp b/src/library/equations_compiler/unbounded_rec.cpp
index 474722a50b..dd5b25a0a0 100644
--- a/src/library/equations_compiler/unbounded_rec.cpp
+++ b/src/library/equations_compiler/unbounded_rec.cpp
@@ -36,10 +36,10 @@ static expr replace_rec_apps(type_context & ctx, expr const & e) {
 
 eqn_compiler_result unbounded_rec(environment & env, options const & opts,
                    metavar_context & mctx, local_context const & lctx,
-                   expr const & e) {
+                   expr const & e, elaborator & elab) {
     type_context ctx(env, opts, mctx, lctx, transparency_mode::Semireducible);
     expr e1 = replace_rec_apps(ctx, e);
-    auto R = elim_match(env, opts, mctx, lctx, e1);
+    auto R = elim_match(env, opts, mctx, lctx, e1, elab);
 
     list<expr> counter_examples;
     if (R.m_counter_examples) {
diff --git a/src/library/equations_compiler/unbounded_rec.h b/src/library/equations_compiler/unbounded_rec.h
index 283a051cff..1589617265 100644
--- a/src/library/equations_compiler/unbounded_rec.h
+++ b/src/library/equations_compiler/unbounded_rec.h
@@ -8,11 +8,12 @@ Author: Leonardo de Moura
 #include "library/type_context.h"
 #include "library/equations_compiler/util.h"
 namespace lean {
+class elaborator;
 /** \brief Eliminate "recursive calls" using rec_fn_macro.
 
     This compilation step can only be used to compile meta definitions.
     If we use it on regular definitions, the kernel will reject it. */
 eqn_compiler_result unbounded_rec(environment & env, options const & opts,
                    metavar_context & mctx, local_context const & lctx,
-                   expr const & eqns);
+                   expr const & eqns, elaborator & elab);
 }
diff --git a/src/library/equations_compiler/wf_rec.cpp b/src/library/equations_compiler/wf_rec.cpp
index 427a24e51a..a5e724c6a3 100644
--- a/src/library/equations_compiler/wf_rec.cpp
+++ b/src/library/equations_compiler/wf_rec.cpp
@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "library/pp_options.h"
 #include "library/app_builder.h"
 #include "library/aux_definition.h"
+#include "frontends/lean/elaborator.h"
 #include "library/replace_visitor_with_tc.h"
 #include "library/vm/vm.h"
 #include "library/vm/vm_list.h"
@@ -33,6 +34,7 @@ struct wf_rec_fn {
     options          m_opts;
     metavar_context  m_mctx;
     local_context    m_lctx;
+    elaborator &     m_elab;
 
     expr             m_ref;
     equations_header m_header;
@@ -43,8 +45,9 @@ struct wf_rec_fn {
     expr             m_dec_tac;
 
     wf_rec_fn(environment const & env, options const & opts,
-              metavar_context const & mctx, local_context const & lctx):
-        m_env(env), m_opts(opts), m_mctx(mctx), m_lctx(lctx) {
+              metavar_context const & mctx, local_context const & lctx,
+              elaborator & elab):
+        m_env(env), m_opts(opts), m_mctx(mctx), m_lctx(lctx), m_elab(elab) {
     }
 
     type_context mk_type_context(local_context const & lctx) {
@@ -154,18 +157,48 @@ struct wf_rec_fn {
             metavar_context mctx = m_ctx.mctx();
             tactic_state s = mk_tactic_state_for(m_parent.m_env, m_parent.m_opts,
                                                  name(m_fn_name, "_wf_rec_mk_dec_tactic"), mctx, m_ctx.lctx(), y_R_x);
-            vm_obj r = tactic_evaluator(m_ctx, m_parent.m_opts, ref)(m_parent.m_dec_tac, s);
-            if (auto new_s = tactic::is_success(r)) {
-                mctx = new_s->mctx();
-                bool postpone_push_delayed = true;
-                expr r = mctx.instantiate_mvars(new_s->main(), postpone_push_delayed);
-                m_parent.m_env = new_s->env();
-                m_ctx.set_env(new_s->env());
-                m_ctx.set_mctx(mctx);
-                return r;
+            try {
+                vm_obj r = tactic_evaluator(m_ctx, m_parent.m_opts, ref)(m_parent.m_dec_tac, s);
+                if (auto new_s = tactic::is_success(r)) {
+                    mctx = new_s->mctx();
+                    bool postpone_push_delayed = true;
+                    expr r = mctx.instantiate_mvars(new_s->main(), postpone_push_delayed);
+                    m_parent.m_env = new_s->env();
+                    m_ctx.set_env(new_s->env());
+                    m_ctx.set_mctx(mctx);
+                    return r;
+                }
+            } catch (elaborator_exception & ex) {
+                bool using_well_founded = is_wf_equations(m_parent.m_ref);
+                auto R = m_parent.m_R;
+                nested_exception ex2(
+                    ex.get_pos(),
+                    [=](formatter const & fmt) {
+                        format r;
+                        formatter _fmt = fmt;
+                        if (is_app_of(R, get_has_well_founded_r_name())) {
+                            options o = fmt.get_options();
+                            o         = o.update_if_undef(get_pp_implicit_name(), true);
+                            _fmt      = fmt.update_options(o);
+                        }
+                        r += format("failed to prove recursive application is decreasing, well founded relation");
+                        r += pp_indent_expr(_fmt, R);
+                        if (!using_well_founded) {
+                            r += line() + format("Possible solutions: ");
+                            r += line() + format("  - Use 'using_well_founded' keyword in the end of your definition "
+                                                "to specify tactics for synthesizing well founded relations and "
+                                                "decreasing proofs.");
+                            r += line() + format("  - The default decreasing tactic uses the 'assumption' tactic, "
+                                                "thus hints (aka local proofs) can be provided using 'have'-expressions.");
+                        }
+                        r += line() + format("The nested exception contains the failure state for the decreasing tactic.");
+                        return r;
+                    },
+                    ex);
+                if (!m_parent.m_elab.try_report(ex2)) throw ex2;
             }
 
-            throw generic_exception(ref, "failed to show recursive call is descreasing");
+            return m_parent.m_elab.mk_sorry(y_R_x);
         }
 
         virtual expr visit_app(expr const & e) {
@@ -517,40 +550,11 @@ struct wf_rec_fn {
         init(eqns, wf_tacs);
 
         /* Eliminate recursion using functional. */
-        try {
-            eqns = elim_recursion(eqns);
-        } catch (exception_with_pos & ex) {
-            expr R = m_R;
-            bool using_well_founded = is_wf_equations(eqns);
-            throw nested_exception(
-                ex.get_pos(),
-                [=](formatter const & fmt) {
-                    format r;
-                    formatter _fmt = fmt;
-                    if (is_app_of(R, get_has_well_founded_r_name())) {
-                        options o = fmt.get_options();
-                        o         = o.update_if_undef(get_pp_implicit_name(), true);
-                        _fmt      = fmt.update_options(o);
-                    }
-                    r += format("failed to prove recursive application is decreasing, well founded relation");
-                    r += pp_indent_expr(_fmt, R);
-                    if (!using_well_founded) {
-                        r += line() + format("Possible solutions: ");
-                        r += line() + format("  - Use 'using_well_founded' keyword in the end of your definition "
-                                             "to specify tactics for synthesizing well founded relations and "
-                                             "decreasing proofs.");
-                        r += line() + format("  - The default decreasing tactic uses the 'assumption' tactic, "
-                                             "thus hints (aka local proofs) can be provided using 'have'-expressions.");
-                    }
-                    r += line() + format("The nested exception contains the failure state for the decreasing tactic.");
-                    return r;
-                },
-                ex);
-        }
+        eqns = elim_recursion(eqns);
         trace_debug_wf(tout() << "after elim_recursion\n" << eqns << "\n";);
 
         /* Eliminate pattern matching */
-        elim_match_result r = elim_match(m_env, m_opts, m_mctx, m_lctx, eqns);
+        elim_match_result r = elim_match(m_env, m_opts, m_mctx, m_lctx, eqns, m_elab);
         expr fn = mk_fix_aux_function(get_equations_header(eqns), r.m_fn);
 
         trace_debug_wf(tout() << "after mk_fix\n" << fn << " :\n  " << mk_type_context().infer(fn) << "\n";);
@@ -567,8 +571,8 @@ struct wf_rec_fn {
     If successful, elim_match is used to compile pattern matching. */
 eqn_compiler_result wf_rec(environment & env, options const & opts,
             metavar_context & mctx, local_context const & lctx,
-            expr const & eqns) {
-    wf_rec_fn proc(env, opts, mctx, lctx);
+            expr const & eqns, elaborator & elab) {
+    wf_rec_fn proc(env, opts, mctx, lctx, elab);
     auto r = proc(eqns);
     env    = proc.m_env;
     mctx   = proc.m_mctx;
diff --git a/src/library/equations_compiler/wf_rec.h b/src/library/equations_compiler/wf_rec.h
index b9a458869a..b3dce8ed77 100644
--- a/src/library/equations_compiler/wf_rec.h
+++ b/src/library/equations_compiler/wf_rec.h
@@ -8,9 +8,10 @@ Author: Leonardo de Moura
 #include "library/type_context.h"
 #include "library/equations_compiler/util.h"
 namespace lean {
+class elaborator;
 eqn_compiler_result wf_rec(environment & env, options const & opts,
             metavar_context & mctx, local_context const & lctx,
-            expr const & eqns);
+            expr const & eqns, elaborator & elab);
 void initialize_wf_rec();
 void finalize_wf_rec();
 }
diff --git a/tests/lean/1162.lean.expected.out b/tests/lean/1162.lean.expected.out
index f8ab5643f8..ca190c0186 100644
--- a/tests/lean/1162.lean.expected.out
+++ b/tests/lean/1162.lean.expected.out
@@ -1 +1,3 @@
 1162.lean:10:12: error: equation compiler error, equation #2 has not been used in the compilation, note that the left-hand-side of equation #1 is a variable
+1162.lean:11:12: error: equation compiler error, equation #3 has not been used in the compilation, note that the left-hand-side of equation #1 is a variable
+1162.lean:12:12: error: equation compiler error, equation #4 has not been used in the compilation, note that the left-hand-side of equation #1 is a variable
diff --git a/tests/lean/elab_error_recovery.lean b/tests/lean/elab_error_recovery.lean
index 6af7671eb0..6bfb9d213c 100644
--- a/tests/lean/elab_error_recovery.lean
+++ b/tests/lean/elab_error_recovery.lean
@@ -9,7 +9,8 @@ def half_baked : ℕ → ℕ
 -- exceptions during tactic evaluation
 | 7  := by do undefined
 -- nested elaboration errors
-| _  := begin exact [] end
+| 10 := begin exact [] end
+-- missing cases
 
 #print half_baked._main
 
diff --git a/tests/lean/elab_error_recovery.lean.expected.out b/tests/lean/elab_error_recovery.lean.expected.out
index a534cfb10d..b9f8043761 100644
--- a/tests/lean/elab_error_recovery.lean.expected.out
+++ b/tests/lean/elab_error_recovery.lean.expected.out
@@ -19,8 +19,7 @@ elab_error_recovery.lean:12:20: error: invalid type ascription, expression has t
 but is expected to have type
   ℕ
 state:
-half_baked : ℕ → ℕ,
-_x : ℕ
+half_baked : ℕ → ℕ
 ⊢ ℕ
 elab_error_recovery.lean:6:8: error: don't know how to synthesize placeholder
 context:
@@ -30,15 +29,18 @@ elab_error_recovery.lean:8:29: error: don't know how to synthesize placeholder
 context:
 half_baked : ℕ → ℕ
 ⊢ ℕ
+elab_error_recovery.lean:1:4: error: non-exhaustive match, the following cases are missing:
+half_baked _
 def half_baked._main : ℕ → ℕ :=
 λ (a : ℕ),
   ite (a = 3) (id_rhs ℕ 2)
     (ite (a = 0) (id_rhs ℕ (1 + ⁇))
        (ite (a = 5) (id_rhs ℕ (⁇ + 4))
-          (ite (a = 42) (id_rhs ℕ (ite (2 ∈ 3) 3 ⁇)) (ite (a = 7) (id_rhs ℕ ⁇) (id_rhs ℕ ⁇)))))
+          (ite (a = 42) (id_rhs ℕ (ite (2 ∈ 3) 3 ⁇))
+             (ite (a = 7) (id_rhs ℕ ⁇) (ite (a = 10) (id_rhs ℕ ⁇) ⁇)))))
 2
 nat.succ (nat.succ (nat.succ (nat.succ ⁇)))
 2
-elab_error_recovery.lean:21:13: error: type expected at
+elab_error_recovery.lean:22:13: error: type expected at
   0
 ∀ (x : ⁇), x = x : Prop