From 9e37e3b9695a214040c52082b1e7288df9362b33 Mon Sep 17 00:00:00 2001
From: ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 24 Oct 2013 17:28:00 +0000
Subject: 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
---
 kernel/sorts.ml | 15 ++++++++++++++-
 1 file changed, 14 insertions(+), 1 deletion(-)

(limited to 'kernel/sorts.ml')

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
-- 
cgit v1.2.3