diff options
| author | Matthieu Sozeau | 2015-11-27 20:34:51 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-11-27 21:01:59 +0100 |
| commit | 4a11dc25938f3f009e23f1e7c5fe01b2558928c3 (patch) | |
| tree | b9e68a7ff2082b25dd4ebc113d43ec9d0f691aa5 /test-suite | |
| parent | a0e72610a71e086da392c8563c2eec2e35211afa (diff) | |
Univs: entirely disallow instantiation of polymorphic constants with
Prop levels.
As they are typed assuming all variables are >= Set now, and this was
breaking an invariant in typing. Only one instance in the standard
library was used in Hurkens, which can be avoided easily. This also
avoids displaying unnecessary >= Set constraints everywhere.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/4287.v | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/test-suite/bugs/closed/4287.v b/test-suite/bugs/closed/4287.v index 0623cf5b84..43c9b51295 100644 --- a/test-suite/bugs/closed/4287.v +++ b/test-suite/bugs/closed/4287.v @@ -118,8 +118,6 @@ Definition setle (B : Type@{i}) := let foo (A : Type@{j}) := A in foo B. Fail Check @setlt@{j Prop}. -Check @setlt@{Prop j}. -Check @setle@{Prop j}. - Fail Definition foo := @setle@{j Prop}. -Definition foo := @setle@{Prop j}. +Check setlt@{Set i}. +Check setlt@{Set j}.
\ No newline at end of file |