diff options
| author | Gaëtan Gilbert | 2020-01-27 13:29:18 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-01-27 13:29:18 +0100 |
| commit | 458cf1324163821b60ab0b731a60bb1977576d9f (patch) | |
| tree | 447f35851e86707b4eacc6dc8feebf1e8cf725be /kernel/type_errors.mli | |
| parent | 506b35913103c17e4d27663aa0f977452d5815b0 (diff) | |
Small API additions to kernel/univ
- allow viewing the internal representation of uglobal and universe
(with universe, this replaces the "map" function. I kept exists and
for_all as they felt somewhat convenient)
- add universe set and map modules (currently unused but they're natural)
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions