diff options
author | 2013-03-21 10:37:07 +0000 | |
---|---|---|
committer | 2013-03-21 10:37:07 +0000 | |
commit | feb933b32c436fc0d04f9390f63edcad0e55cfee (patch) | |
tree | b3b64130bc0f886c77400f570b2a658dc967d4db /printing/printmod.ml | |
parent | 4d060e768ced36ad915daf8e651191a06a802bb3 (diff) |
Printmod: fresh fake namespaces for non-visible modules (fix #2668, #2983)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16328 85f007b7-540e-0410-9357-904b9bb8a0f7
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))); |