diff options
| author | Maxime Dénès | 2015-10-15 14:38:57 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2015-10-15 14:38:57 +0200 |
| commit | ba8dd1c47bcbbcd2678eca78783db7f5c95f37e7 (patch) | |
| tree | d7cba397b0f9e6ece420352b5dfba877e713d421 | |
| parent | 44817bf722eacb0379bebc7e435bfafa503d574f (diff) | |
Test file for #4346: Set is no longer of type Type
| -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 0000000000..b50dff2411 --- /dev/null +++ b/test-suite/bugs/closed/4346.v @@ -0,0 +1,2 @@ +Check (Set <: Type). +Check (Set <<: Type). |