Extra removal

Author: robsimmons

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -250,9 +250,6 @@ partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit :=
 
 @[builtin_tactic skip] def evalSkip : Tactic := fun _ => pure ()
 
-@[builtin_tactic unknown] def evalUnknown : Tactic := fun stx => do
-  addCompletionInfo <| CompletionInfo.tactic stx
-
 @[builtin_tactic failIfSuccess] def evalFailIfSuccess : Tactic := fun stx =>
   Term.withoutErrToSorry <| withoutRecover do
     let tactic := stx[1]