diff options
| author | Matthieu Sozeau | 2015-06-23 17:08:38 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-06-26 16:26:59 +0200 |
| commit | a0b48c4d55cd18655d8e79e6d66b0a0a0651fe3d (patch) | |
| tree | caed8f3c87d0aaab1ece708ef452094ae0353ce7 /kernel/sorts.ml | |
| parent | d9ac4c22a3a6543959d413120304e356d625c0f9 (diff) | |
Share prop/set values in sorts.ml.
Diffstat (limited to 'kernel/sorts.ml')
| -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 6e6f41e821..e2854abfd3 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 = |