diff options
author | 2015-11-27 20:34:51 +0100 | |
---|---|---|
committer | 2015-11-27 21:01:59 +0100 | |
commit | 4a11dc25938f3f009e23f1e7c5fe01b2558928c3 (patch) | |
tree | b9e68a7ff2082b25dd4ebc113d43ec9d0f691aa5 /test-suite/bugs/closed | |
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/bugs/closed')
-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 0623cf5b8..43c9b5129 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 |