From 49a764bd81ac1b21130d54a1808ce95b9992a36d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 3 Mar 2014 13:46:59 +0100
Subject: Removing generic hashes in kernel.

---
 kernel/constr.ml | 65 +++++++++++++++++++++++++++++---------------------------
 1 file changed, 34 insertions(+), 31 deletions(-)

(limited to 'kernel/constr.ml')

diff --git a/kernel/constr.ml b/kernel/constr.ml
index 61718a7f7b..826c7f6437 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -715,37 +715,40 @@ let rec hash t =
 and hash_term_array t =
   Array.fold_left (fun acc t -> combine (hash t) acc) 0 t
 
-module Hcaseinfo =
-  Hashcons.Make(
-    struct
-      type t = case_info
-      type u = inductive -> inductive
-      let hashcons hind ci = { ci with ci_ind = hind ci.ci_ind }
-      let pp_info_equal info1 info2 =
-        Int.equal info1.ind_nargs info2.ind_nargs &&
-        info1.style == info2.style
-      let equal ci ci' =
-	ci.ci_ind == ci'.ci_ind &&
-	Int.equal ci.ci_npar ci'.ci_npar &&
-	Array.equal Int.equal ci.ci_cstr_ndecls ci'.ci_cstr_ndecls && (* we use [Array.equal] on purpose *)
-	pp_info_equal ci.ci_pp_info ci'.ci_pp_info  (* we use (=) on purpose *)
-      open Hashset.Combine
-      let hash_pp_info info =
-        let h = match info.style with
-        | LetStyle -> 0
-        | IfStyle -> 1
-        | LetPatternStyle -> 2
-        | MatchStyle -> 3
-        | RegularStyle -> 4
-        in
-        combine info.ind_nargs h
-      let hash ci =
-        let h1 = ind_hash ci.ci_ind in
-        let h2 = Int.hash ci.ci_npar in
-        let h3 = Array.fold_left combine 0 ci.ci_cstr_ndecls in
-        let h4 = hash_pp_info ci.ci_pp_info in
-        combine4 h1 h2 h3 h4
-    end)
+module CaseinfoHash =
+struct
+  type t = case_info
+  type u = inductive -> inductive
+  let hashcons hind ci = { ci with ci_ind = hind ci.ci_ind }
+  let pp_info_equal info1 info2 =
+    Int.equal info1.ind_nargs info2.ind_nargs &&
+    info1.style == info2.style
+  let equal ci ci' =
+    ci.ci_ind == ci'.ci_ind &&
+    Int.equal ci.ci_npar ci'.ci_npar &&
+    Array.equal Int.equal ci.ci_cstr_ndecls ci'.ci_cstr_ndecls && (* we use [Array.equal] on purpose *)
+    pp_info_equal ci.ci_pp_info ci'.ci_pp_info  (* we use (=) on purpose *)
+  open Hashset.Combine
+  let hash_pp_info info =
+    let h = match info.style with
+    | LetStyle -> 0
+    | IfStyle -> 1
+    | LetPatternStyle -> 2
+    | MatchStyle -> 3
+    | RegularStyle -> 4
+    in
+    combine info.ind_nargs h
+  let hash ci =
+    let h1 = ind_hash ci.ci_ind in
+    let h2 = Int.hash ci.ci_npar in
+    let h3 = Array.fold_left combine 0 ci.ci_cstr_ndecls in
+    let h4 = hash_pp_info ci.ci_pp_info in
+    combine4 h1 h2 h3 h4
+end
+
+module Hcaseinfo = Hashcons.Make(CaseinfoHash)
+
+let case_info_hash = CaseinfoHash.hash
 
 let hcons_caseinfo = Hashcons.simple_hcons Hcaseinfo.generate hcons_ind
 
-- 
cgit v1.2.3