From 8c107d6936ae735b3f3ed1747f10410ff7c7ed2f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 2 May 2015 16:01:25 -0700
Subject: [PATCH] fix(frontends/lean/builtin_cmds): bug in `export` command

Cause: we have two different tokes to represent declarations: [decls] and [declarations]

fixes #568
---
 src/frontends/lean/builtin_cmds.cpp |  2 ++
 tests/lean/run/568.lean             | 15 +++++++++++++++
 2 files changed, 17 insertions(+)
 create mode 100644 tests/lean/run/568.lean

diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 73619ae8c..fd7ab27f9 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -602,6 +602,8 @@ static void parse_metaclasses(parser & p, buffer<name> & r) {
         while (p.curr_is_token(get_lbracket_tk())) {
             name m = parse_metaclass(p);
             tmp.erase_elem(m);
+            if (m == get_declarations_tk())
+                tmp.erase_elem(get_decls_tk());
         }
         r.append(tmp);
     } else {
diff --git a/tests/lean/run/568.lean b/tests/lean/run/568.lean
new file mode 100644
index 000000000..d79773020
--- /dev/null
+++ b/tests/lean/run/568.lean
@@ -0,0 +1,15 @@
+namespace f1
+  definition flip := 20
+end f1
+
+namespace f2
+  definition flip := 10
+end f2
+
+namespace f3
+  export [declarations] f1
+  export -[declarations] f2
+end f3
+
+export [declarations] f1
+export -[declarations] f2