diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-06-23 17:08:38 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-06-26 16:26:59 +0200 |
| commit | a0b48c4d55cd18655d8e79e6d66b0a0a0651fe3d (patch) | |
| tree | caed8f3c87d0aaab1ece708ef452094ae0353ce7 | |
| parent | d9ac4c22a3a6543959d413120304e356d625c0f9 (diff) | |
Share prop/set values in 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 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 = |