diff options
| author | Matthieu Sozeau | 2014-09-04 11:24:40 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-04 11:28:28 +0200 |
| commit | 84916b37627cce78a313f850ecbcff1c3b8c3d49 (patch) | |
| tree | cbe69729218326516618c53d90122cd5b489b846 /kernel/declarations.mli | |
| parent | 1c3340c10b56ba821fe381f1e89bcfd48a04121e (diff) | |
Fix bug #3559, ensuring a canonical order of universe level quantifications when
introducing constants (e.g. Top.1 is always before Top.2), compatible with the one
used before introduction of hMaps in LMap/LSet.
Diffstat (limited to 'kernel/declarations.mli')
0 files changed, 0 insertions, 0 deletions