From d8fa93b4a2f6437a6718bd4503301579f2e617c6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 31 May 2017 15:10:07 -0700
Subject: [PATCH] feat(library/init/meta/tactic): add dependent parameters for
 empty introv

---
 library/init/meta/tactic.lean | 2 +-
 tests/lean/run/introv.lean    | 7 +++++++
 2 files changed, 8 insertions(+), 1 deletion(-)

diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 05da86fd19..b4c5adfa67 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -522,7 +522,7 @@ do t ← target,
    end
 
 meta def introv : list name → tactic (list expr)
-| []      := return []
+| []      := intros_dep
 | (n::ns) := do hs ← intros_dep, h ← intro n, hs' ← introv ns, return (hs ++ h :: hs')
 
 /-- Returns n fully qualified if it refers to a constant, or else fails. -/
diff --git a/tests/lean/run/introv.lean b/tests/lean/run/introv.lean
index 3d2ac75322..ccf21f1e41 100644
--- a/tests/lean/run/introv.lean
+++ b/tests/lean/run/introv.lean
@@ -9,3 +9,10 @@ begin
   introv h₁ h₂,
   exact h₁.trans h₂
 end
+
+example : ∀ a b : nat, a = b → b = a :=
+begin
+  introv,
+  intro h,
+  exact h.symm
+end