diff options
Diffstat (limited to 'printing/printmod.ml')
| -rw-r--r-- | printing/printmod.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml index 0c28e64f6..e9fc35e2f 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -69,8 +69,15 @@ let print_kn locals kn = with Not_found -> print_modpath locals kn +(** Each time we have to print a non-globally visible structure, + we place its elements in a fake fresh namespace. *) + +let mk_fake_top = + let r = ref 0 in + fun () -> incr r; Id.of_string ("FAKETOP"^(string_of_int !r)) + let nametab_register_dir mp = - let id = Id.of_string "FAKETOP" in + let id = mk_fake_top () in let fp = Libnames.make_path DirPath.empty id in let dir = DirPath.make [id] in Nametab.push_dir (Nametab.Until 1) dir (DirModule (dir,(mp,DirPath.empty))); |