Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 18 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/2603.v b/test-suite/bugs/closed/shouldsucceed/2603.v
new file mode 100644
index 00000000..a556b9bf
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2603.v
@@ -0,0 +1,18 @@
+Module Type T.
+End T.
+
+Declare Module K : T.
+
+Module Type L.
+Declare Module E : T.
+End L.
+
+Module M1 : L with Module E:=K.
+Module E := K.
+Fail Inductive t := E. (* Used to be accepted, but End M1 below was failing *)
+End M1.
+
+Module M2 : L with Module E:=K.
+Inductive t := E.
+Fail Module E := K. (* Used to be accepted *)
+Fail End M2. (* Used to be accepted *)