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

fix(frontends/lean): another bug in sections with parameters

Browse source
This commit is contained in:
Leonardo de Moura 2015-04-21 19:50:21 -07:00
parent 3df99e514b
commit fe9f4dd95f
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/builtin_cmds.cpp
View file

@ -274,7 +274,7 @@ static void redeclare_aliases(parser & p,
list<pair<name, level>> old_level_entries, list<pair<name, level>> old_level_entries,
list<pair<name, expr>> old_entries) { list<pair<name, expr>> old_entries) {
environment const & env = p.env(); environment const & env = p.env();
if (!in_context(env)) if (!in_context(env) && !in_section(env))
return; return;
list<pair<name, expr>> new_entries = p.get_local_entries(); list<pair<name, expr>> new_entries = p.get_local_entries();
buffer<pair<name, expr>> to_redeclare; buffer<pair<name, expr>> to_redeclare;

2
tests/lean/run/section4.lean
View file

@ -7,7 +7,7 @@ section
universe k universe k
parameter A : Type parameter A : Type
context section
universe variable l universe variable l
universe variable u universe variable u
parameter B : Type parameter B : Type