From d6958be7e77737e9f9af817acfcb562357b4b089 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 5 Feb 2015 10:50:40 -0800
Subject: [PATCH] fix(library/tactic/location): replace cache must not be used
 when only a subset of all occurrences should be replaced at
 replace_occurrences

---
 src/library/tactic/location.cpp | 3 ++-
 tests/lean/run/rewrite5.lean    | 9 +++++++++
 2 files changed, 11 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/rewrite5.lean

diff --git a/src/library/tactic/location.cpp b/src/library/tactic/location.cpp
index 8dfd0a0ee..aa3b615bd 100644
--- a/src/library/tactic/location.cpp
+++ b/src/library/tactic/location.cpp
@@ -113,6 +113,7 @@ deserializer & operator>>(deserializer & d, location & loc) {
 }
 
 expr replace_occurrences(expr const & e, expr const & t, occurrence const & occ, unsigned idx) {
+    bool use_cache   = occ.is_all();
     unsigned occ_idx = 0;
     return replace(e, [&](expr const & e, unsigned offset) {
             if (e == t) {
@@ -121,6 +122,6 @@ expr replace_occurrences(expr const & e, expr const & t, occurrence const & occ,
                     return some_expr(mk_var(offset+idx));
             }
             return none_expr();
-        });
+        }, use_cache);
 }
 }
diff --git a/tests/lean/run/rewrite5.lean b/tests/lean/run/rewrite5.lean
new file mode 100644
index 000000000..826274e78
--- /dev/null
+++ b/tests/lean/run/rewrite5.lean
@@ -0,0 +1,9 @@
+import algebra.group
+open algebra
+
+variable {A : Type}
+variable [s : group A]
+include s
+
+theorem mul.right_inv (a : A) : a * a⁻¹ = 1 :=
+by rewrite ⟨-{a}inv_inv at {1}, mul.left_inv⟩