From 4eab11ec3dd90a693bc5472b01a2cd229b5ab877 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 30 May 2017 19:02:25 +0200 Subject: [PATCH] fix(frontends/lean/structure_cmd): even less error recovery --- src/frontends/lean/structure_cmd.cpp | 2 ++ tests/lean/structure_elab_segfault.lean | 1 + tests/lean/structure_elab_segfault.lean.expected.out | 2 ++ 3 files changed, 5 insertions(+) diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 2585b61195..9609b01342 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -507,6 +507,8 @@ struct structure_cmd_fn { /** \brief elaborate parameters and "parent" types */ void elaborate_header() { + auto _ = m_p.no_error_recovery_scope(); // we require that m_p.elaborate_type(mk_let()) is a let, etc. + buffer include_vars; m_p.get_include_variables(include_vars); buffer tmp_locals; diff --git a/tests/lean/structure_elab_segfault.lean b/tests/lean/structure_elab_segfault.lean index 92aea08c95..f20931298d 100644 --- a/tests/lean/structure_elab_segfault.lean +++ b/tests/lean/structure_elab_segfault.lean @@ -1 +1,2 @@ +structure foo {A} (R) (x : list A) : Prop := (bar : R x) structure test : Type := (f : ∀ x y, true) diff --git a/tests/lean/structure_elab_segfault.lean.expected.out b/tests/lean/structure_elab_segfault.lean.expected.out index 1e8434c1f3..f9978b5314 100644 --- a/tests/lean/structure_elab_segfault.lean.expected.out +++ b/tests/lean/structure_elab_segfault.lean.expected.out @@ -1,2 +1,4 @@ structure_elab_segfault.lean:1:0: error: infer type failed, sort expected delayed[?m_1] +structure_elab_segfault.lean:2:0: error: infer type failed, sort expected + delayed[?m_1]