From 0b995c4fe3cda9b31a74bbd224079111c6e7af0d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 30 Apr 2015 18:22:58 -0700
Subject: [PATCH] fix(library/tactic/rewrite_tactic): relax reducibility
 constraints in some parts of the rewrite tactic

fixes #567
---
 src/library/tactic/rewrite_tactic.cpp | 10 +++++-----
 tests/lean/run/567.lean               |  6 ++++++
 2 files changed, 11 insertions(+), 5 deletions(-)
 create mode 100644 tests/lean/run/567.lean

diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/tactic/rewrite_tactic.cpp
index 8118b9a94..165297e0a 100644
--- a/src/library/tactic/rewrite_tactic.cpp
+++ b/src/library/tactic/rewrite_tactic.cpp
@@ -1206,8 +1206,8 @@ class rewrite_fn {
             expr Pb  = instantiate(Px, vidx, b);
 
             expr A   = m_tc->infer(a).first;
-            level l1 = sort_level(m_tc->ensure_type(Pa).first);
-            level l2 = sort_level(m_tc->ensure_type(A).first);
+            level l1 = sort_level(m_unifier_tc->ensure_type(Pa).first);
+            level l2 = sort_level(m_unifier_tc->ensure_type(A).first);
             expr H;
             if (has_dep_elim) {
                 expr Haeqx = mk_app(mk_constant(get_eq_name(), {l1}), A, a, mk_var(0));
@@ -1257,8 +1257,8 @@ class rewrite_fn {
             expr Px  = replace_occurrences(Pa, a, occ, vidx);
             expr Pb  = instantiate(Px, vidx, b);
             expr A   = m_tc->infer(a).first;
-            level l1 = sort_level(m_tc->ensure_type(Pa).first);
-            level l2 = sort_level(m_tc->ensure_type(A).first);
+            level l1 = sort_level(m_unifier_tc->ensure_type(Pa).first);
+            level l2 = sort_level(m_unifier_tc->ensure_type(A).first);
             expr M   = m_g.mk_meta(m_ngen.next(), Pb);
             expr H;
             if (has_dep_elim) {
@@ -1476,7 +1476,7 @@ public:
                     process_failure(elem, false);
                     return proof_state_seq();
                 }
-            } catch (kernel_exception &) {
+            } catch (kernel_exception & ex) {
                 process_failure(elem, true);
                 return proof_state_seq();
             }
diff --git a/tests/lean/run/567.lean b/tests/lean/run/567.lean
new file mode 100644
index 000000000..2fcda8269
--- /dev/null
+++ b/tests/lean/run/567.lean
@@ -0,0 +1,6 @@
+import data.set
+
+example {A : Type} (H : set A) (a x : A) (p : a = x) (l : H x) : H a :=
+begin
+  rewrite p, exact l
+end