diff options
| author | Jason Gross | 2017-04-11 09:50:55 -0400 |
|---|---|---|
| committer | Jason Gross | 2017-04-25 15:13:25 -0400 |
| commit | 12f34b2ebfcbe958ba53b49399c3fcaf01f7a18c (patch) | |
| tree | 28ed8ee557334749d73bf95d20ea91372445933e /plugins | |
| parent | 84845f766d9b9d532f615352fbc8a0e78e1727e9 (diff) | |
Generalize cache_term_by_tactic_then
This will allow a cache_term tactic that doesn't suffer from the
Not_found anomalies of abstract in typeclass resolution.
Diffstat (limited to 'plugins')
0 files changed, 0 insertions, 0 deletions