Commit 2025-07-31 12:13 b451018e

chore: deprecate cc tactic (#27710) This PR deprecates Mathlib's cc tactic. (This is a port of Leo's implementation in Lean 3.) While cc does support some goals which grind doesn't (some by design for performance reasons, others we should catch up soon anyway), Mathlib hasn't ever relied on this additional functionality, and we don't know of downstream libraries using it. If we discover such users, I'd like to first have a change to migrate them to grind, and then we can decide whether to cancel the deprecation, or spin out cc into a standalone library.