From 862d23f6b631f27acca50d7f0e1e2bcfed810611 Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Mon, 29 May 2017 11:59:11 -0400
Subject: [PATCH] fix(library/init/meta/interactive): disallow wildcard in
 rewrite

---
 library/init/meta/interactive.lean |  9 +++------
 tests/lean/rw_wildcard.lean        | 11 -----------
 2 files changed, 3 insertions(+), 17 deletions(-)
 delete mode 100644 tests/lean/rw_wildcard.lean

diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index a3a5431323..9b37ae90b1 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -360,12 +360,9 @@ meta def rw_rules : parser rw_rules_t :=
 
 private meta def rw_core (m : transparency) (rs : parse rw_rules) (loca : parse location) : tactic unit :=
 match loca with
-| loc.wildcard :=
-do ls ← local_context,
-   let ls_names := list.map (fun (l : expr), l.local_pp_name) ls,
-   ls_names.mfor' (fun loc, try $ rw_hyp m rs.rules loc)
-| loc.ns [] := rw_goal m rs.rules
-| loc.ns hs := rw_hyps m rs.rules hs
+| loc.wildcard := fail "wildcard not allowed with rewrite"
+| loc.ns []    := rw_goal m rs.rules
+| loc.ns hs    := rw_hyps m rs.rules hs
 end >> try (reflexivity reducible)
     >> (returnopt rs.end_pos >>= save_info <|> skip)
 
diff --git a/tests/lean/rw_wildcard.lean b/tests/lean/rw_wildcard.lean
deleted file mode 100644
index 012614673b..0000000000
--- a/tests/lean/rw_wildcard.lean
+++ /dev/null
@@ -1,11 +0,0 @@
-lemma rw_wild_card :
-forall (a b c a' b' c' : nat),
-(0 + a) = a' ->
-(0 + b) = b' ->
-(0 + c) = c' ->
-a' + b' + c' = a + b + c :=
-begin
-    intros,
-    rewrite [add_comm, add_zero] at *,
-    rewrite [a_1, a_2, a_3]
-end