diff options
| author | Pierre-Marie Pédrot | 2020-06-16 16:18:09 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-06-16 16:29:25 +0200 |
| commit | 1ef9819b9b52e8f9a537c070e2642845be0d0315 (patch) | |
| tree | c92e004130a0b990a07cf078934172e23e193cf0 /kernel/type_errors.ml | |
| parent | 31cbaf0fe258438948ba9611d599dc456c313ddd (diff) | |
Use evar clauses instead of meta clauses in Autorewrite hint registration.
This is barely more meaningful but at least we do not rely on an antiquated
API now.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions