feat(library/init/meta/tactic): add dependent parameters for empty introv

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. -/

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