From 4a11dc25938f3f009e23f1e7c5fe01b2558928c3 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 27 Nov 2015 20:34:51 +0100 Subject: 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. --- theories/Classes/CMorphisms.v | 14 ++------------ 1 file changed, 2 insertions(+), 12 deletions(-) (limited to 'theories/Classes') 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 -- cgit v1.2.3