From 61254847fba910afb1dfd50c7a8449a7601921e9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 20 Feb 2017 14:51:59 -0800 Subject: [PATCH] fix(frontends/lean/structure_cmd): when error recovery is enabled, we must not assume the expression in the fixed line is a binding expression (it may be a `sorry` expression) --- src/frontends/lean/structure_cmd.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 249945f7e7..7698261a6b 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -323,6 +323,8 @@ struct structure_cmd_fn { */ expr update_locals(expr new_tmp, buffer & locals) { for (unsigned i = 0; i < locals.size(); i++) { + if (!is_binding(new_tmp)) + throw exception("structure command elaboration was interrupted due to nested errors"); expr new_local = mk_local(mlocal_name(locals[i]), binding_name(new_tmp), binding_domain(new_tmp), binding_info(new_tmp)); locals[i] = new_local;