Commit 2021-10-05 16:47 1c502ee3

View on Github →

chore: remove block tactic (#58) This is included upstream now.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/List/Basic.lean

Modified Mathlib/Data/Nat/Basic.lean

Modified Mathlib/Init/Algebra/Functions.lean

Modified Mathlib/Init/Data/Nat/Lemmas.lean

Modified Mathlib/Logic/Basic.lean

Modified Mathlib/Logic/Function/Basic.lean

Modified Mathlib/Tactic/Basic.lean

Deleted Mathlib/Tactic/Block.lean

deleted def Lean.Elab.Tactic.closeAllOrAdmit

deleted def Lean.Elab.Tactic.focusAndBlock

Modified Mathlib/Test/Split.lean