diff options
| -rw-r--r-- | kernel/sorts.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/sorts.ml b/kernel/sorts.ml index 6e6f41e82..e2854abfd 100644 --- a/kernel/sorts.ml +++ b/kernel/sorts.ml @@ -26,8 +26,8 @@ let univ_of_sort = function | Prop Null -> Universe.type0m let sort_of_univ u = - if is_type0m_univ u then Prop Null - else if is_type0_univ u then Prop Pos + if is_type0m_univ u then prop + else if is_type0_univ u then set else Type u let compare s1 s2 = |