diff options
| author | Pierre-Marie Pédrot | 2020-06-08 15:17:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-06-19 16:02:25 +0200 |
| commit | 21b4e41544f03de18d9f5b1bdb93a26b36a97999 (patch) | |
| tree | 85e1848df45b189ad40693ebe2b651eae9ba2c1f /kernel/type_errors.ml | |
| parent | 2a24a665ca63d82ce2576e75636ab6fdbcad9b36 (diff) | |
Opacify the type of hint metadata.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions