diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-11-27 20:34:51 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-11-27 21:01:59 +0100 |
| commit | 4a11dc25938f3f009e23f1e7c5fe01b2558928c3 (patch) | |
| tree | b9e68a7ff2082b25dd4ebc113d43ec9d0f691aa5 /theories/Logic/ClassicalFacts.v | |
| 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 'theories/Logic/ClassicalFacts.v')
| -rw-r--r-- | theories/Logic/ClassicalFacts.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index 6f736e45f..cdc3e0461 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -658,4 +658,3 @@ Proof. exists x; intro; exact Hx. exists x0; exact Hnot. Qed. - |