diff options
| author | Pierre-Marie Pédrot | 2014-03-01 14:17:09 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-03-05 21:23:14 +0100 |
| commit | 2a0d260c9c80c07844605fcb6844bb9cfdfeb0fd (patch) | |
| tree | 6330bc8c76a73a514d0b93c76de6c1fe79cc947d /kernel/names.ml | |
| parent | 073e4a3fc9748268c2b4e5549e54d894c6fe74cd (diff) | |
Canary testing absence of generic equality for KerNames
Diffstat (limited to 'kernel/names.ml')
| -rw-r--r-- | kernel/names.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index b0c9335348..21d22baffb 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -332,6 +332,7 @@ module MPmap = CMap.Make(ModPath) module KerName = struct type t = { + canary : Canary.t; modpath : ModPath.t; dirpath : DirPath.t; knlabel : Label.t; @@ -339,14 +340,16 @@ module KerName = struct (** Lazily computed hash. If unset, it is set to negative values. *) } + let canary = Canary.obj + type kernel_name = t let make modpath dirpath knlabel = - { modpath; dirpath; knlabel; refhash = -1; } + { modpath; dirpath; knlabel; refhash = -1; canary; } let repr kn = (kn.modpath, kn.dirpath, kn.knlabel) let make2 modpath knlabel = - { modpath; dirpath = DirPath.empty; knlabel; refhash = -1; } + { modpath; dirpath = DirPath.empty; knlabel; refhash = -1; canary; } let modpath kn = kn.modpath let label kn = kn.knlabel @@ -391,7 +394,7 @@ module KerName = struct * (string -> string) let hashcons (hmod,hdir,hstr) kn = let { modpath = mp; dirpath = dp; knlabel = l; refhash; } = kn in - { modpath = hmod mp; dirpath = hdir dp; knlabel = hstr l; refhash; } + { modpath = hmod mp; dirpath = hdir dp; knlabel = hstr l; refhash; canary; } let equal kn1 kn2 = kn1.modpath == kn2.modpath && kn1.dirpath == kn2.dirpath && kn1.knlabel == kn2.knlabel |