From 28a2641df29cd7530c3ebe329dc118ba3f444b10 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 2 Mar 2014 20:40:16 +0100 Subject: Fixing generic hashes and replacing them with proper ones. --- kernel/nativelambda.ml | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) (limited to 'kernel/nativelambda.ml') diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index e6a579c5bf..a757f013a8 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -473,18 +473,27 @@ let empty_args = [||] module Renv = struct + module ConstrHash = + struct + type t = constructor + let equal = eq_constructor + let hash = constructor_hash + end + + module ConstrTable = Hashtbl.Make(ConstrHash) + type constructor_info = tag * int * int (* nparam nrealargs *) type t = { name_rel : name Vect.t; - construct_tbl : (constructor, constructor_info) Hashtbl.t; + construct_tbl : constructor_info ConstrTable.t; } let make () = { name_rel = Vect.make 16 Anonymous; - construct_tbl = Hashtbl.create 111 + construct_tbl = ConstrTable.create 111 } let push_rel env id = Vect.push env.name_rel id @@ -501,7 +510,7 @@ module Renv = Lrel (Vect.get_last env.name_rel (n-1), n) let get_construct_info env c = - try Hashtbl.find env.construct_tbl c + try ConstrTable.find env.construct_tbl c with Not_found -> let ((mind,j), i) = c in let oib = lookup_mind mind !global_env in @@ -509,7 +518,7 @@ module Renv = let tag,arity = oip.mind_reloc_tbl.(i-1) in let nparams = oib.mind_nparams in let r = (tag, nparams, arity) in - Hashtbl.add env.construct_tbl c r; + ConstrTable.add env.construct_tbl c r; r end -- cgit v1.2.3