diff options
| author | Gaëtan Gilbert | 2019-10-13 16:35:47 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-14 10:24:26 +0200 |
| commit | afd214869f050d07f9774d770c289bdc6e602dfd (patch) | |
| tree | 7b5518a714466c675e6ca152bdb78e865510a369 /printing/printmod.ml | |
| parent | c3479eceb8e07b37570a80bca9937e3520c61024 (diff) | |
Remove obj_sec field of Nametab.obj_prefix record.
There are no more users.
Diffstat (limited to 'printing/printmod.ml')
| -rw-r--r-- | printing/printmod.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml index 03921bca30..4cc6bc2052 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -213,7 +213,7 @@ let print_kn locals kn = let nametab_register_dir obj_mp = let id = mk_fake_top () in let obj_dir = DirPath.make [id] in - Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirModule { obj_dir; obj_mp; obj_sec = DirPath.empty })) + Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirModule { obj_dir; obj_mp; })) (** Nota: the [global_reference] we register in the nametab below might differ from internal ones, since we cannot recreate here |