max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(frontends/lean/parser): remove unnecessary restriction

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-07 11:40:39 -07:00
parent 1e6b3614ab
commit b9c62af37d
1 changed files with 0 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/frontends/lean/parser.cpp
View file

@ -1792,9 +1792,6 @@ expr parser::patexpr_to_pattern(expr const & pat_or_expr, bool skip_main_fn, buf
}
expr parser::parse_pattern_or_expr(unsigned rbp) {
if (m_in_quote) {
throw parser_error("patterns cannot occur inside of quoted terms", pos());
}
all_id_local_scope scope(*this);
return parse_expr(rbp);
}