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/Classes | |
| 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/Classes')
| -rw-r--r-- | theories/Classes/CMorphisms.v | 14 |
1 files changed, 2 insertions, 12 deletions
diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v index fdedbf672..b13671cec 100644 --- a/theories/Classes/CMorphisms.v +++ b/theories/Classes/CMorphisms.v @@ -269,16 +269,6 @@ Section GenericInstances. Unset Strict Universe Declaration. (** The complement of a crelation conserves its proper elements. *) - Program Definition complement_proper (A : Type@{k}) (RA : crelation A) - `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) : - Proper (RA ==> RA ==> iff) (complement@{i j Prop} R) := _. - - Next Obligation. - Proof. - unfold complement. - pose (mR x y X x0 y0 X0). - intuition. - Qed. (** The [flip] too, actually the [flip] instance is a bit more general. *) Program Definition flip_proper @@ -521,8 +511,8 @@ Ltac proper_reflexive := Hint Extern 1 (subrelation (flip _) _) => class_apply @flip1 : typeclass_instances. Hint Extern 1 (subrelation _ (flip _)) => class_apply @flip2 : typeclass_instances. -Hint Extern 1 (Proper _ (complement _)) => apply @complement_proper - : typeclass_instances. +(* Hint Extern 1 (Proper _ (complement _)) => apply @complement_proper *) +(* : typeclass_instances. *) Hint Extern 1 (Proper _ (flip _)) => apply @flip_proper : typeclass_instances. Hint Extern 2 (@Proper _ (flip _) _) => class_apply @proper_flip_proper |