From 995ab20edbc52deb41166e6ef31539234aaf5c00 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 12 Oct 2011 09:15:45 +0000
Subject: test-suite: non-regression test for bug #2603

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14556 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/bugs/closed/shouldsucceed/2603.v | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 test-suite/bugs/closed/shouldsucceed/2603.v

diff --git a/test-suite/bugs/closed/shouldsucceed/2603.v b/test-suite/bugs/closed/shouldsucceed/2603.v
new file mode 100644
index 0000000000..a556b9bf40
--- /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 *)
-- 
cgit v1.2.3