diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-10-15 14:38:57 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-10-15 14:38:57 +0200 |
| commit | ba8dd1c47bcbbcd2678eca78783db7f5c95f37e7 (patch) | |
| tree | d7cba397b0f9e6ece420352b5dfba877e713d421 /test-suite/bugs/closed/4346.v | |
| parent | 44817bf722eacb0379bebc7e435bfafa503d574f (diff) | |
Test file for #4346: Set is no longer of type Type
Diffstat (limited to 'test-suite/bugs/closed/4346.v')
| -rw-r--r-- | test-suite/bugs/closed/4346.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/4346.v b/test-suite/bugs/closed/4346.v new file mode 100644 index 000000000..b50dff241 --- /dev/null +++ b/test-suite/bugs/closed/4346.v @@ -0,0 +1,2 @@ +Check (Set <: Type). +Check (Set <<: Type). |