From 65a514ad8a1d5bbfad05363094bdc8867804b5ea Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 24 Oct 2013 19:04:06 -0700 Subject: [PATCH] fix(frontends/lean/parser): option propagation Signed-off-by: Leonardo de Moura --- src/frontends/lean/parser.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index bae34bd95..1883f3802 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1538,7 +1538,7 @@ class parser::imp { formatter fmt = m_frontend.get_state().get_formatter(); options opts = m_frontend.get_state().get_options(); lean_pos_info_provider pos_provider(*this); - regular(m_frontend) << ex.get_justification().pp(fmt, opts, &pos_provider, true) << endl; + regular(m_frontend) << mk_pair(ex.get_justification().pp(fmt, opts, &pos_provider, true), opts) << endl; } void updt_options() {