From de8a71bc5b2cd846eb3c3bd9b8b6b70ad8def79e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 4 Sep 2014 11:25:41 -0700 Subject: [PATCH] perf(frontends/lean): do not create extra_info annotation when we are not collecting info Signed-off-by: Leonardo de Moura --- src/frontends/lean/builtin_exprs.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 69e0c6320a..4768eca23c 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -364,7 +364,10 @@ static expr parse_sorry(parser & p, unsigned, expr const *, pos_info const & pos } static expr parse_rparen(parser & p, unsigned, expr const * args, pos_info const & pos) { - return p.save_pos(mk_extra_info(args[0]), pos); + if (p.collecting_info()) + return p.save_pos(mk_extra_info(args[0]), pos); + else + return args[0]; } parse_table init_nud_table() {