diff options
| author | Gaëtan Gilbert | 2018-10-10 14:08:08 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-10-16 15:52:53 +0200 |
| commit | da049e138e2b1acf9cdd40d3dbac4508f76f21cb (patch) | |
| tree | d3fc16c340bece88e617f716cbf16637578afa63 /kernel/type_errors.ml | |
| parent | bab144fed76c452c49c95c87682d442df68b82f2 (diff) | |
Deprecate UnivGen.new_{univ,Type,Type_sort}
They are impractical since we need to get the level out to register it
afterwards.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions