michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

perf(frontends/lean): do not create extra_info annotation when we are not collecting info

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-09-04 11:25:41 -07:00
parent d76218e9d1
commit de8a71bc5b
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/frontends/lean/builtin_exprs.cpp
View file

@ -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() {