diff options
Diffstat (limited to 'test-suite/bugs/closed/2923.v')
-rw-r--r-- | test-suite/bugs/closed/2923.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/2923.v b/test-suite/bugs/closed/2923.v new file mode 100644 index 00000000..8a0003a3 --- /dev/null +++ b/test-suite/bugs/closed/2923.v @@ -0,0 +1,12 @@ +Module Type SIGNATURE1. + Inductive IndType: Set := + | AConstructor. +End SIGNATURE1. + +Module Type SIGNATURE2. + Declare Module M1: SIGNATURE1. +End SIGNATURE2. + +Module M2 (Module M1_: SIGNATURE1) : SIGNATURE2. + Module M1 := M1_. +End M2. |