Skip to content

Commit cb84f90

Browse files
committed
chore: move cc to another repository (leanprover-community#34669)
`cc` tactic is replaced by `grind` and deprecated since 2025-07-31, so I created the repository [Komyyy/legacy-cc](https://github.com/Komyyy/legacy-cc) and move `cc` tactic to there. Co-authored-by: Komyyy <pol_tta@outlook.jp>
1 parent c8e5e59 commit cb84f90

10 files changed

Lines changed: 0 additions & 3870 deletions

File tree

Mathlib.lean

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -6610,11 +6610,6 @@ public import Mathlib.Tactic.Bound.Attribute
66106610
public import Mathlib.Tactic.Bound.Init
66116611
public import Mathlib.Tactic.ByCases
66126612
public import Mathlib.Tactic.ByContra
6613-
public import Mathlib.Tactic.CC
6614-
public import Mathlib.Tactic.CC.Addition
6615-
public import Mathlib.Tactic.CC.Datatypes
6616-
public import Mathlib.Tactic.CC.Lemmas
6617-
public import Mathlib.Tactic.CC.MkProof
66186613
public import Mathlib.Tactic.CancelDenoms
66196614
public import Mathlib.Tactic.CancelDenoms.Core
66206615
public import Mathlib.Tactic.Cases

Mathlib/Tactic.lean

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -17,11 +17,6 @@ public import Mathlib.Tactic.Bound.Attribute
1717
public import Mathlib.Tactic.Bound.Init
1818
public import Mathlib.Tactic.ByCases
1919
public import Mathlib.Tactic.ByContra
20-
public import Mathlib.Tactic.CC
21-
public import Mathlib.Tactic.CC.Addition
22-
public import Mathlib.Tactic.CC.Datatypes
23-
public import Mathlib.Tactic.CC.Lemmas
24-
public import Mathlib.Tactic.CC.MkProof
2520
public import Mathlib.Tactic.CancelDenoms
2621
public import Mathlib.Tactic.CancelDenoms.Core
2722
public import Mathlib.Tactic.Cases

Mathlib/Tactic/CC.lean

Lines changed: 0 additions & 277 deletions
This file was deleted.

0 commit comments

Comments
 (0)