diff options
| author | Pierre-Marie Pédrot | 2020-04-04 17:04:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-12-14 09:54:46 +0100 |
| commit | 981146bbc716494ba9ced0d6b403923b293cdec1 (patch) | |
| tree | dd74ec6343737c31e7a00acd3779a5bff9a5527c /tactics/hints.ml | |
| parent | d0667eb4a165c065b0d64069641ca0cd39d62219 (diff) | |
Cache meta access in meta_instance.
Diffstat (limited to 'tactics/hints.ml')
0 files changed, 0 insertions, 0 deletions