diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-07-31 18:53:21 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-03-22 11:35:46 +0100 |
| commit | 920f1548e9245ddfc8b923c5039a5e09dc0c87d4 (patch) | |
| tree | 802bb5a85dc733eb5ea6f4b0a72dcf4127dec2f1 /kernel/univ.ml | |
| parent | 09c2011fbdbb2ac1ce33e5abe52d93b907b21a3c (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/univ.ml')
0 files changed, 0 insertions, 0 deletions