Commit 2023-10-12 10:52 560cd074

refactor: No need for CachedData in library_search and rw? (#7305) Previously, Mathlib.Tactic.Cache defined a CachedData data structure to keep a reference to the CompactedRegion that we get when unpickling the cache from a file, but it was never used. It also seems to be the case that keeping that reference is not necessary to keep the unpickled data alive. (It is the other way around: The data stays alive until .free is called explicitly, which we do not plan to do here.) Therefore, to simplify the code, this PR removes CachedData. This came out of working on #find in #6363