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 | |
| 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')
| -rw-r--r-- | kernel/univ.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index b2f251283e..202f6232da 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -368,6 +368,10 @@ module Level = struct let c = Int.compare (hash u) (hash v) in if c == 0 then RawLevel.compare (data u) (data v) else c + + let natural_compare u v = + if u == v then 0 + else RawLevel.compare (data u) (data v) let to_string x = match data x with @@ -1896,8 +1900,11 @@ struct let univs = Array.fold_left fold univs v in (univs, cst) + let sort_levels a = + Array.sort Level.natural_compare a; a + let to_context (ctx, cst) = - (Instance.of_array (Array.of_list (LSet.elements ctx)), cst) + (Instance.of_array (sort_levels (Array.of_list (LSet.elements ctx))), cst) let of_context (ctx, cst) = (Instance.levels ctx, cst) |