From f556da10a117396c2c796f6915321b67849f65cd Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 31 Jul 2015 18:53:21 +0200 Subject: Adding eq/compare/hash for syntactic view at constant/inductive/constructor kernel_name pairs rather than viewing them from only the user or canonical part. Hopefully more uniformity in Constr.hasheq (using systematically == on subterms). A semantic change: Cooking now indexing again on full pairs of kernel names rather than only on the canonical names, so as to preserve user name. Also, in pair of kernel names, ensuring the compact representation is used as soon as both names are the same. --- kernel/cooking.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'kernel/cooking.ml') diff --git a/kernel/cooking.ml b/kernel/cooking.ml index be71bd7b4..9849f156c 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -44,15 +44,15 @@ module RefHash = struct type t = my_global_reference let equal gr1 gr2 = match gr1, gr2 with - | ConstRef c1, ConstRef c2 -> Constant.CanOrd.equal c1 c2 - | IndRef i1, IndRef i2 -> eq_ind i1 i2 - | ConstructRef c1, ConstructRef c2 -> eq_constructor c1 c2 + | ConstRef c1, ConstRef c2 -> Constant.SyntacticOrd.equal c1 c2 + | IndRef i1, IndRef i2 -> eq_syntactic_ind i1 i2 + | ConstructRef c1, ConstructRef c2 -> eq_syntactic_constructor c1 c2 | _ -> false open Hashset.Combine let hash = function - | ConstRef c -> combinesmall 1 (Constant.hash c) - | IndRef i -> combinesmall 2 (ind_hash i) - | ConstructRef c -> combinesmall 3 (constructor_hash c) + | ConstRef c -> combinesmall 1 (Constant.SyntacticOrd.hash c) + | IndRef i -> combinesmall 2 (ind_syntactic_hash i) + | ConstructRef c -> combinesmall 3 (constructor_syntactic_hash c) end module RefTable = Hashtbl.Make(RefHash) -- cgit v1.2.3