diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-07-31 18:53:21 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-08-02 19:13:50 +0200 |
| commit | f556da10a117396c2c796f6915321b67849f65cd (patch) | |
| tree | d8d9285813189d3a3eee3f5173297521ae2be089 /kernel/cooking.ml | |
| parent | d8226295e6237a43de33475f798c3c8ac6ac4866 (diff) | |
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.
Diffstat (limited to 'kernel/cooking.ml')
| -rw-r--r-- | kernel/cooking.ml | 12 |
1 files changed, 6 insertions, 6 deletions
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) |