diff options
| -rw-r--r-- | printing/printmod.ml | 9 | ||||
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2668.v | 6 | ||||
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2983.v | 8 |
3 files changed, 22 insertions, 1 deletions
diff --git a/printing/printmod.ml b/printing/printmod.ml index 0c28e64f6d..e9fc35e2f6 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))); diff --git a/test-suite/bugs/closed/shouldsucceed/2668.v b/test-suite/bugs/closed/shouldsucceed/2668.v new file mode 100644 index 0000000000..74c8fa347b --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2668.v @@ -0,0 +1,6 @@ +Require Import MSetPositive. +Require Import MSetProperties. + +Module Pos := MSetPositive.PositiveSet. +Module PPPP := MSetProperties.WPropertiesOn(Pos). +Print Module PPPP.
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/2983.v b/test-suite/bugs/closed/shouldsucceed/2983.v new file mode 100644 index 0000000000..15598352b1 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2983.v @@ -0,0 +1,8 @@ +Module Type ModA. +End ModA. +Module Type ModB(A : ModA). +End ModB. +Module Foo(A : ModA)(B : ModB A). +End Foo. + +Print Module Foo.
\ No newline at end of file |