diff options
| author | Pierre-Marie Pédrot | 2014-07-21 19:42:44 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-07-21 19:51:16 +0200 |
| commit | 3007da7147d86f2e85347b9e70c1faea7d2eed06 (patch) | |
| tree | 3347971b532ef69f63c4a370c716629cd9ef1fa1 /kernel/type_errors.ml | |
| parent | 5519c14ed70d231d369e56b0792e6c43423bae10 (diff) | |
Universe level maps use HMaps.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions