From 43fa75f7a9c179bf64bb4e9482f336bc1b0cb8fb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 14 Jul 2014 03:36:06 +0100 Subject: [PATCH] fix(frontends/lean/decl_cmds): typo Signed-off-by: Leonardo de Moura --- src/frontends/lean/decl_cmds.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 7bae639b47..af13c74789 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -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));