diff options
| author | Gaëtan Gilbert | 2019-10-13 20:20:56 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-13 20:20:56 +0200 |
| commit | ce1d51dc40cdb65b01b559ab076f76b265ccf6c4 (patch) | |
| tree | f3b0697a4ba47561024cef230d9b44895cc7d0de /test-suite | |
| parent | 7f039cac07526881da1a149b8c0e49be32c2e89e (diff) | |
Fix #10888: Context import behaviour in modtype
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_10888.v | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_10888.v b/test-suite/bugs/closed/bug_10888.v new file mode 100644 index 0000000000..3c2e8011d7 --- /dev/null +++ b/test-suite/bugs/closed/bug_10888.v @@ -0,0 +1,11 @@ + +Module Type T. +Context {A:Type}. +End T. + +Module M(X:T). + Import X. + Check X.A. + Check A. + Definition B := A. +End M. |