From eab9321a3b287550de19f0d8603299c27cceff01 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 8 Oct 2014 13:12:42 -0700
Subject: [PATCH] fix(frontends/lean): make all variables/parameters visible
 for 'variables' command

---
 src/frontends/lean/decl_cmds.cpp |  2 +-
 tests/lean/run/mor.lean          | 15 +++++++++++++++
 2 files changed, 16 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/mor.lean

diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index d749c3b65..7b91b5586 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -203,7 +203,7 @@ static environment variables_cmd_core(parser & p, variable_kind k) {
         expr type = p.parse_expr();
         p.parse_close_binder_info(bi);
         level_param_names ls = to_level_param_names(collect_univ_params(type));
-        list<expr> ctx = locals_to_context(type, p);
+        list<expr> ctx = p.locals_to_context();
         for (auto id : ids) {
             // Hack: to make sure we get different universe parameters for each parameter.
             // Alternative: elaborate once and copy types replacing universes in new_ls.
diff --git a/tests/lean/run/mor.lean b/tests/lean/run/mor.lean
new file mode 100644
index 000000000..06e0646a0
--- /dev/null
+++ b/tests/lean/run/mor.lean
@@ -0,0 +1,15 @@
+-- Copyright (c) 2014 Floris van Doorn. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Floris van Doorn
+
+import algebra.category
+
+open eq eq.ops category
+
+namespace morphism
+  section
+  parameter {ob : Type}
+  parameter {C : category ob}
+  variables {a b c d : ob} {h : mor c d} {g : mor b c} {f : mor a b}
+  end
+end morphism