Specializing hash functions for widely used types.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16933 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 14 insertions, 1 deletions

diff --git a/kernel/sorts.ml b/kernel/sorts.ml
index d2469c4fd..04deade92 100644
--- a/kernel/sorts.ml
+++ b/kernel/sorts.ml
@@ -46,6 +46,19 @@ let family = function
 
 let family_equal = (==)
 
+open Hashset.Combine
+
+let hash = function
+| Prop p ->
+  let h = match p with
+  | Pos -> 0
+  | Null -> 1
+  in
+  combinesmall 1 h
+| Type u ->
+  let h = Universe.hash u in
+  combinesmall 2 h
+
 module Hsorts =
   Hashcons.Make(
     struct
@@ -59,7 +72,7 @@ module Hsorts =
         | (Prop c1, Prop c2) -> c1 == c2
         | (Type u1, Type u2) -> u1 == u2
         |_ -> false
-      let hash = Hashtbl.hash
+      let hash = hash
     end)
 
 let hcons = Hashcons.simple_hcons Hsorts.generate hcons_univ