diff options
| author | Pierre-Marie Pédrot | 2020-12-11 18:41:48 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-11 12:59:41 +0100 |
| commit | 5c69eb442ac6b007854462066c38c3ec2556e311 (patch) | |
| tree | 3907a1e6ec066f62871dcadc7a1350fa20173ee1 /kernel/nativecode.ml | |
| parent | ffb482f0c18bff2c65dcc9cd2b65bd20b398245d (diff) | |
Use the Evarutil cache for Class_tactics.evar_dependencies.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions