1 files changed, 0 insertions, 29 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/3008.v b/test-suite/bugs/closed/shouldsucceed/3008.v
deleted file mode 100644
index 3f3a979a..00000000
--- a/test-suite/bugs/closed/shouldsucceed/3008.v
+++ /dev/null
@@ -1,29 +0,0 @@
-Module Type Intf1.
-Parameter T : Type.
-Inductive a := A.
-End Intf1.
-
-Module Impl1 <: Intf1.
-Definition T := unit.
-Inductive a := A.
-End Impl1.
-
-Module Type Intf2
-  (Impl1 : Intf1).
-Parameter x : Impl1.A=Impl1.A -> Impl1.T.
-End Intf2.
-
-Module Type Intf3
-  (Impl1 : Intf1)
-  (Impl2 : Intf2(Impl1)).
-End Intf3.
-
-Fail Module Toto
-  (Impl1' : Intf1)
-  (Impl2 : Intf2(Impl1'))
-  (Impl3 : Intf3(Impl1)(Impl2)).
-(* A UserError is expected here, not an uncaught Not_found *)
-
-(* NB : the Inductive above and the A=A weren't in the initial test,
-   they are here only to force an access to the environment
-   (cf [Printer.qualid_of_global]) and check that this env is ok. *)
-\ No newline at end of file