From 143143e94c7c3fc7803cd7abeeaa3b5c920c44ff Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 1 Feb 2015 10:38:30 -0800
Subject: [PATCH] fix(library/tactic/inversion_tactic): missing normalization
 step in the inversion_tactic

---
 src/library/tactic/inversion_tactic.cpp |  2 +-
 tests/lean/run/sigma_match.lean         | 28 +++++++++++++++++++++++++
 2 files changed, 29 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/sigma_match.lean

diff --git a/src/library/tactic/inversion_tactic.cpp b/src/library/tactic/inversion_tactic.cpp
index 4292409ad..c7f861fd7 100644
--- a/src/library/tactic/inversion_tactic.cpp
+++ b/src/library/tactic/inversion_tactic.cpp
@@ -359,7 +359,7 @@ class inversion_tac {
         buffer<expr> hyps;
         g.get_hyps(hyps);
         expr const & h      = hyps.back();
-        expr const & h_type = mlocal_type(h);
+        expr const & h_type = m_tc.whnf(mlocal_type(h)).first;
         buffer<expr> I_args;
         expr const & I      = get_app_args(h_type, I_args);
         name const & I_name = const_name(I);
diff --git a/tests/lean/run/sigma_match.lean b/tests/lean/run/sigma_match.lean
new file mode 100644
index 000000000..606166a96
--- /dev/null
+++ b/tests/lean/run/sigma_match.lean
@@ -0,0 +1,28 @@
+open sigma
+
+constant hom.{l₁ l₂} {A : Type.{l₁}} {B : Type.{l₂}} (a : A) (b : B) : Type.{max l₁ l₂}
+
+definition arrow_ob [reducible] (A B : Type) : Type :=
+Σ (a : A) (b : B), hom a b
+
+definition src1 {A B : Type} (x : arrow_ob A B) : A :=
+match x with
+  ⟨a, b, h⟩ := a
+end
+
+definition src2 {A B : Type} : arrow_ob A B → A,
+src2 ⟨a, _, _⟩ := a
+
+definition src3 {A B : Type} (x : arrow_ob A B) : A :=
+match x with
+  ⟨a, _, _⟩ := a
+end
+
+example (A B : Type) (x : arrow_ob A B) : src1 x = src2 x :=
+rfl
+
+example (A B : Type) (x : arrow_ob A B) : src1 x = src3 x :=
+rfl
+
+example (A B : Type) (x : arrow_ob A B) : src2 x = src3 x :=
+rfl