diff options
| author | Matthieu Sozeau | 2015-09-23 16:09:14 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-02 15:54:10 +0200 |
| commit | e841deb4750d43ab19f91907476d75fc73860c5a (patch) | |
| tree | b92b71db1d0a33864f8a0a1aa72f247a2f91b88a /kernel/nativecode.ml | |
| parent | cc69a4697633e14fc00c9bd0858b38120645464b (diff) | |
Univs (kernel) adapt to new invariants
Remove predicative flag and adapt to new invariant where every universe
must be declared, ensuring it is >= Set, safe_repr is not necessary
anymore.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions