diff options
| author | Emilio Jesus Gallego Arias | 2018-10-31 09:39:53 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-31 12:58:02 +0100 |
| commit | 0adc2073cf3e7bd3b2d9ee2cdf75e16e3a243c44 (patch) | |
| tree | 5d7212f3462f7e650238906768a4bfd199ec9091 /library/libnames.ml | |
| parent | e29dc5ab5e85eb5f740de83f9f0b97b233651a3e (diff) | |
[nametab] Move global_dir_reference to Nametab
This type is "private" to the Nametab, which manages it. It thus makes
sense IMHO to live there.
Diffstat (limited to 'library/libnames.ml')
| -rw-r--r-- | library/libnames.ml | 14 |
1 files changed, 0 insertions, 14 deletions
diff --git a/library/libnames.ml b/library/libnames.ml index f6fc5ed4b7..d2c96d4163 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -168,25 +168,11 @@ type object_prefix = { obj_sec : DirPath.t; } -(* to this type are mapped DirPath.t's in the nametab *) -type global_dir_reference = - | DirOpenModule of object_prefix - | DirOpenModtype of object_prefix - | DirOpenSection of object_prefix - | DirModule of object_prefix - 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 -| DirOpenModtype op1, DirOpenModtype op2 -> eq_op op1 op2 -| DirOpenSection op1, DirOpenSection op2 -> eq_op op1 op2 -| DirModule op1, DirModule op2 -> eq_op op1 op2 -| _ -> false - (* Default paths *) let default_library = Names.DirPath.initial (* = ["Top"] *) |