fix(library/tactic/intros_tactic): seg fault at intros tactic, fixes #366

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;

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