From 2c18da20b260c55d8da49b1bb4f53e72dbc75a87 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Wed, 24 Apr 2019 11:37:42 +0000
Subject: Revert #9249

---
 test-suite/output/Notations4.out |  2 --
 test-suite/output/Notations4.v   | 17 -----------------
 2 files changed, 19 deletions(-)

(limited to 'test-suite')

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.
-- 
cgit v1.2.3