diff options
| author | Pierre-Marie Pédrot | 2014-04-20 23:05:41 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-04-20 23:05:41 +0200 |
| commit | 7a79b6dd25db742d37d14d2531f4cb14d53fc6bf (patch) | |
| tree | 5c34ce4c819cfab7ec98c2ac00a1002640c71849 | |
| parent | 87b42716ade692cd8ea27703bb6406af8d95849a (diff) | |
Adding a test for bug #2923.
| -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 0000000000..8a0003a397 --- /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. |