From d1eaa7bcda588ebdd1a90b311ecfbd65d5d7642d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 28 Jun 2015 11:45:30 -0700
Subject: [PATCH] feat(frontends/lean/parse_rewrite_tactic): accept trailing
 comman in rewrite tactic

see issue #695
---
 src/frontends/lean/parse_rewrite_tactic.cpp | 4 ++--
 tests/lean/run/695d.lean                    | 7 +++++++
 2 files changed, 9 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/695d.lean

diff --git a/src/frontends/lean/parse_rewrite_tactic.cpp b/src/frontends/lean/parse_rewrite_tactic.cpp
index 766195b90..6080071af 100644
--- a/src/frontends/lean/parse_rewrite_tactic.cpp
+++ b/src/frontends/lean/parse_rewrite_tactic.cpp
@@ -135,14 +135,14 @@ static expr parse_rewrite_element(parser & p, bool use_paren) {
 void parse_rewrite_tactic_elems(parser & p, buffer<expr> & elems) {
     if (p.curr_is_token(get_lbracket_tk())) {
         p.next();
-        while (true) {
+        while (!p.curr_is_token(get_rbracket_tk())) {
             auto pos = p.pos();
             elems.push_back(p.save_pos(parse_rewrite_element(p, false), pos));
             if (!p.curr_is_token(get_comma_tk()))
                 break;
             p.next();
         }
-        p.check_token_next(get_rbracket_tk(), "invalid rewrite tactic, ',' or ']' expected");
+        p.next();
     } else {
         auto pos = p.pos();
         elems.push_back(p.save_pos(parse_rewrite_element(p, true), pos));
diff --git a/tests/lean/run/695d.lean b/tests/lean/run/695d.lean
new file mode 100644
index 000000000..19fed078b
--- /dev/null
+++ b/tests/lean/run/695d.lean
@@ -0,0 +1,7 @@
+import data.nat
+open nat
+
+example (a b : nat) : 0 + a + 0 = a :=
+begin
+  rewrite [add_zero, zero_add,]
+end