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

fix(frontends/lean/decl_cmds): typo

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-14 03:36:06 +01:00
parent fab7934265
commit 43fa75f7a9
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -350,11 +350,10 @@ static environment variables_cmd(parser & p) {
ls = append(ls, new_ls);
environment env = p.env();
for (auto id : ids)
env = declare_var(p, env, id, ls, type, true, bi, pos);
env = declare_var(p, env, id, ls, type, false, bi, pos);
return env;
}
void register_decl_cmds(cmd_table & r) {
add_cmd(r, cmd_info("universe", "declare a global universe level", universe_cmd));
add_cmd(r, cmd_info("variable", "declare a new parameter", variable_cmd));