Commit 2026-02-01 13:22 cb84f90f

View on Github →

chore: move cc to another repository (#34669) cc tactic is replaced by grind and deprecated since 2025-07-31, so I created the repository Komyyy/legacy-cc and move cc tactic to there.

Estimated changes

deleted inductive Mathlib.Tactic.CC.ACApps
deleted structure Mathlib.Tactic.CC.ACEntry
deleted structure Mathlib.Tactic.CC.CCConfig
deleted structure Mathlib.Tactic.CC.CCState
deleted structure Mathlib.Tactic.CC.Entry
deleted inductive Mathlib.Tactic.CC.EntryExpr
deleted structure Mathlib.Tactic.CC.ParentOcc
deleted inductive Foo
deleted def Rel
deleted inductive Vec
deleted theorem ex₁
deleted def ex₂
deleted def foo
deleted def mul'