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 /kernel/uGraph.ml | |
| 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 'kernel/uGraph.ml')
0 files changed, 0 insertions, 0 deletions