2 files changed, 0 insertions, 19 deletions
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 5bf4ec7bfb..ca20575f1a 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -49,8 +49,6 @@ myAnd1 True True
      : Prop
 r 2 3
      : Prop
-Notation Cn := Foo.FooCn
-Expands to: Notation Notations4.J.Mfoo.Foo.Bar.Cn
 let v := 0%test17 in v : myint63
      : myint63
 fun y : nat => # (x, z) |-> y & y
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index b33ad17ed4..3311549013 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -181,23 +181,6 @@ Check r 2 3.
 
 End I.
 
-(* 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.
-
 Require Import Coq.Numbers.Cyclic.Int63.Int63.
 Module NumeralNotations.
   Module Test17.