BUGFIX: Three fixes for the price of 1 in sorts.ml:

- Proper [family] implementation
- Use the tailor made hash function for Sorts.t in two places.

1 files changed, 4 insertions, 2 deletions

diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index ae86d686a..6e6f41e82 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -62,6 +62,8 @@ let is_small = function
 let family = function
   | Prop Null -> InProp
   | Prop Pos -> InSet
+  | Type u when is_type0m_univ u -> InProp
+  | Type u when is_type0_univ u -> InSet
   | Type _ -> InType
 
 let family_equal = (==)
@@ -76,7 +78,7 @@ let hash = function
   in
   combinesmall 1 h
 | Type u ->
-  let h = Hashtbl.hash u in (** FIXME *)
+ let h = Univ.Universe.hash u in
   combinesmall 2 h
 
 module List = struct
@@ -101,7 +103,7 @@ module Hsorts =
         | (Type u1, Type u2) -> u1 == u2
         |_ -> false
 
-      let hash = Hashtbl.hash (** FIXME *)
+      let hash = hash
     end)
 
 let hcons = Hashcons.simple_hcons Hsorts.generate Hsorts.hcons hcons_univ