diff options
Diffstat (limited to 'kernel/uGraph.ml')
| -rw-r--r-- | kernel/uGraph.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index afdc8f1511..064fffe98e 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -921,7 +921,7 @@ let sort_universes g = let types = Array.init (max_lvl + 1) (function | 0 -> Level.prop | 1 -> Level.set - | n -> Level.make mp (n-2)) + | n -> Level.make2 mp (Level.Id.make (n-2))) in let g = Array.fold_left (fun g u -> let g, u = safe_repr g u in |