From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- test-suite/bugs/closed/1576.v | 38 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) create mode 100644 test-suite/bugs/closed/1576.v (limited to 'test-suite/bugs/closed/1576.v') diff --git a/test-suite/bugs/closed/1576.v b/test-suite/bugs/closed/1576.v new file mode 100644 index 00000000..3621f7a1 --- /dev/null +++ b/test-suite/bugs/closed/1576.v @@ -0,0 +1,38 @@ +Module Type TA. +Parameter t : Set. +End TA. + +Module Type TB. +Declare Module A: TA. +End TB. + +Module Type TC. +Declare Module B : TB. +End TC. + +Module Type TD. + +Declare Module B: TB . +Declare Module C: TC + with Module B := B . +End TD. + +Module Type TE. +Declare Module D : TD. +End TE. + +Module Type TF. +Declare Module E: TE. +End TF. + +Module G (D: TD). +Module B' := D.C.B. +End G. + +Module H (F: TF). +Module I := G(F.E.D). +End H. + +Declare Module F: TF. +Module K := H(F). + -- cgit v1.2.3