diff options
| author | Gaëtan Gilbert | 2018-08-28 15:19:13 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-09-13 15:05:57 +0200 |
| commit | cc66d4a0977db4994000bfc7e45937b3ccff3c93 (patch) | |
| tree | d7ef363064917a10b895793a67006ded5775b98b /kernel/indtypes.ml | |
| parent | 230f135eb7ba80b4be74da493f205a7eb1b5fa3d (diff) | |
Avoid repeat universe declarations for constants with split univs
Diffstat (limited to 'kernel/indtypes.ml')
0 files changed, 0 insertions, 0 deletions