From ebda057499d26c6eb5ea274aefa848f7423c6144 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 4 Dec 2014 09:26:10 -0800
Subject: [PATCH] fix(library/tactic/intros_tactic): seg fault at intros
 tactic, fixes #366

---
 src/library/tactic/intros_tactic.cpp | 1 +
 tests/lean/run/366.lean              | 8 ++++++++
 2 files changed, 9 insertions(+)
 create mode 100644 tests/lean/run/366.lean

diff --git a/src/library/tactic/intros_tactic.cpp b/src/library/tactic/intros_tactic.cpp
index 325cfd588..49b676d0c 100644
--- a/src/library/tactic/intros_tactic.cpp
+++ b/src/library/tactic/intros_tactic.cpp
@@ -33,6 +33,7 @@ tactic intros_tactic(list<name> _ns, bool relax_main_opaque) {
                         expr new_t = tc->whnf(t).first;
                         if (!is_pi(new_t))
                             break;
+                        t = new_t;
                     }
                 }
                 name new_name;
diff --git a/tests/lean/run/366.lean b/tests/lean/run/366.lean
new file mode 100644
index 000000000..897344e54
--- /dev/null
+++ b/tests/lean/run/366.lean
@@ -0,0 +1,8 @@
+import hott.path
+open path
+definition foo (A : Type) : Type := Π (a : A), a ≈ a
+definition thm : Π (A : Type), foo A :=
+begin
+  intros,
+  apply idp
+end