From c3ce9d0a2dbe93ff117937bdcdc30e9b8ea377f3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 1 Aug 2016 21:55:41 -0700 Subject: [PATCH] fix(frontends/lean): bug that only happens in newer versions of g++ See #1098 I only managed to reproduce the bug after I installed Ubuntu 16.04 --- src/frontends/lean/elaborator.cpp | 3 ++- src/frontends/lean/old_elaborator.cpp | 3 ++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index aed8f474c1..0bb78ed0e6 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1378,7 +1378,8 @@ void elaborator::invoke_tactics(checkpoint const & C) { if (to_process.empty()) return; unassigned_uvars_to_params(); - scope_elaborate_fn scope(nested_elaborate); + elaborate_fn fn(nested_elaborate); + scope_elaborate_fn scope(fn); unsigned i = to_process.size(); while (i > 0) { diff --git a/src/frontends/lean/old_elaborator.cpp b/src/frontends/lean/old_elaborator.cpp index adb85848b7..638ef0d936 100644 --- a/src/frontends/lean/old_elaborator.cpp +++ b/src/frontends/lean/old_elaborator.cpp @@ -1683,7 +1683,8 @@ static tactic_state to_tactic_state(environment const & env, options const & opt } optional old_elaborator::execute_tactic(expr const & tactic, tactic_state const & s, expr const & mvar) { - scope_elaborate_fn scope(nested_elaborate); + elaborate_fn fn(nested_elaborate); + scope_elaborate_fn scope(fn); name tactic_name("_tactic"); expr tactic_type = ::lean::mk_app(mk_constant("tactic", {mk_level_one()}), mk_constant("unit"));