diff options
| -rw-r--r-- | test-suite/bugs/closed/bug_8951.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_8951.v b/test-suite/bugs/closed/bug_8951.v new file mode 100644 index 0000000000..dce19318c5 --- /dev/null +++ b/test-suite/bugs/closed/bug_8951.v @@ -0,0 +1,14 @@ +Module Type T. + Polymorphic Parameter Inline t@{i} : Type@{i}. +End T. + +Module M. + Polymorphic Definition t@{i} := nat. +End M. + +Module Make (X:T). + Include X. + +End Make. + +Module P := Make M. |