Merge PR #9249: Fixing printing bug due to using equality wrongly checking hash keys of kernel names (or checking wrong hash keys?)

2 files changed, 19 insertions, 0 deletions

diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index d58e4bf2d6..94016e170b 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -45,3 +45,5 @@ fun x : nat => (x.-1)%pred
      : Prop
 ##
      : Prop
+Notation Cn := Foo.FooCn
+Expands to: Notation Top.J.Mfoo.Foo.Bar.Cn
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 61206b6dd0..309115848f 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -164,3 +164,20 @@ Open Scope my_scope.
 Check ##.
 
 End H.
+
+(* Fixing a bug reported by G. Gonthier in #9207 *)
+
+Module J.
+
+Module Import Mfoo.
+Module Foo.
+Definition FooCn := 2.
+Module Bar.
+Notation Cn := FooCn.
+End Bar.
+End Foo.
+Export Foo.Bar.
+End Mfoo.
+About Cn.
+
+End J.