diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-22 01:14:50 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-29 14:59:29 +0100 |
| commit | c408e819ce39b27f0842c84b1b24c585ac5b6086 (patch) | |
| tree | a3dac227a23d098e70c7d74bd719f93f3cc6724c /library/libnames.ml | |
| parent | 437f20f0a1c2717cd7baae52e2ab20750dd9d4fb (diff) | |
[lib] [api] Introduce record for `object_prefix`
This is a minor cleanup adding a record in a try to structure the
state living in `Lib`.
Diffstat (limited to 'library/libnames.ml')
| -rw-r--r-- | library/libnames.ml | 19 |
1 files changed, 12 insertions, 7 deletions
diff --git a/library/libnames.ml b/library/libnames.ml index 81878e72f..a471d8396 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -156,10 +156,15 @@ let qualid_of_dirpath dir = type object_name = full_path * KerName.t -type object_prefix = DirPath.t * (ModPath.t * DirPath.t) +type object_prefix = { + obj_dir : DirPath.t; + obj_mp : ModPath.t; + obj_sec : DirPath.t; +} -let make_oname (dirpath,(mp,dir)) id = - make_path dirpath id, KerName.make mp dir (Label.of_id id) +(* let make_oname (dirpath,(mp,dir)) id = *) +let make_oname { obj_dir; obj_mp; obj_sec } id = + make_path obj_dir id, KerName.make obj_mp obj_sec (Label.of_id id) (* to this type are mapped DirPath.t's in the nametab *) type global_dir_reference = @@ -170,10 +175,10 @@ type global_dir_reference = | DirClosedSection of DirPath.t (* this won't last long I hope! *) -let eq_op (d1, (mp1, p1)) (d2, (mp2, p2)) = - DirPath.equal d1 d2 && - DirPath.equal p1 p2 && - ModPath.equal mp1 mp2 +let eq_op op1 op2 = + DirPath.equal op1.obj_dir op2.obj_dir && + DirPath.equal op1.obj_sec op2.obj_sec && + ModPath.equal op1.obj_mp op2.obj_mp let eq_global_dir_reference r1 r2 = match r1, r2 with | DirOpenModule op1, DirOpenModule op2 -> eq_op op1 op2 |