diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean
index 244538bf39..9b8dbad2c6 100644
--- a/src/Lean/Elab/Tactic/ElabTerm.lean
+++ b/src/Lean/Elab/Tactic/ElabTerm.lean
@@ -101,7 +101,7 @@ def refineCore (stx : Syntax) (tagSuffix : Name) (allowNaturalHoles : Bool) : Ta
 @[builtinTactic «specialize»] def evalSpecialize : Tactic := fun stx => withMainContext do
   match stx with
   | `(tactic| specialize $e:term) =>
-    let (e, mvarIds') ← elabTermWithHoles e (← getMainTarget) `specialize (allowNaturalHoles := true)
+    let (e, mvarIds') ← elabTermWithHoles e none `specialize (allowNaturalHoles := true)
     let h := e.getAppFn
     if h.isFVar then
       let localDecl ← getLocalDecl h.fvarId!
diff --git a/tests/lean/run/specialize2.lean b/tests/lean/run/specialize2.lean
new file mode 100644
index 0000000000..82d5fc0927
--- /dev/null
+++ b/tests/lean/run/specialize2.lean
@@ -0,0 +1,11 @@
+example : (p → q → False) ↔ (¬ p ∨ ¬ q) := by
+  apply Iff.intro
+  . intro h
+    byCases hp:p <;> byCases hq:q
+    . specialize h hp hq; contradiction
+    . exact Or.inr hq
+    . exact Or.inl hp
+    . exact Or.inr hq
+  . intro
+    | Or.inl hnp => intros; contradiction
+    | Or.inr hnq => intros; contradiction