From 3e0aa07cfb1d552e11b37aaf5f0224bfb5b47523 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 23 Jun 2015 17:02:50 +0200
Subject: 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.
---
 kernel/sorts.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index ae86d686ae..6e6f41e821 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
-- 
cgit v1.2.3