- Fix in kernel conversion not folding the universe constraints

correctly when comparing stacks.
- Disallow Type i <= Prop/Set constraints, that would otherwise allow
constraints that make a universe lower than Prop.
- Fix stm/lemmas that was pushing constraints to the global context,
it is done depending on the constant/variable polymorphic status now.
- Adapt generalized rewriting in Type code to these fixes.

2 files changed, 2 insertions, 45 deletions

diff --git a/theories/Classes/CEquivalence.v b/theories/Classes/CEquivalence.v
index b540feabf..8610f18c3 100644
--- a/theories/Classes/CEquivalence.v
+++ b/theories/Classes/CEquivalence.v
@@ -107,11 +107,11 @@ Section Respecting.
 
   Definition respecting `(eqa : Equivalence A (R : crelation A), 
                           eqb : Equivalence B (R' : crelation B)) : Type :=
-    { morph : A -> B | respectful R R' morph morph }.
+    { morph : A -> B & respectful R R' morph morph }.
 
   Program Instance respecting_equiv `(eqa : Equivalence A R, eqb : Equivalence B R') :
     Equivalence (fun (f g : respecting eqa eqb) => 
-                   forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)).
+                   forall (x y : A), R x y -> R' (projT1 f x) (projT1 g y)).
 
   Solve Obligations with unfold respecting in * ; simpl_crelation ; program_simpl.
 
diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
index 4b031f949..b1c2842f7 100644
--- a/theories/Classes/CMorphisms.v
+++ b/theories/Classes/CMorphisms.v
@@ -192,10 +192,6 @@ Section Relations.
     intros. apply sub. apply mor.
   Qed.
 
-  Global Instance proper_subrelation_proper :
-    Proper (subrelation ++> eq ==> impl) (@Proper A).
-  Proof. reduce. subst. firstorder. Qed.
-
   Global Instance proper_subrelation_proper_arrow :
     Proper (subrelation ++> eq ==> arrow) (@Proper A).
   Proof. reduce. subst. firstorder. Qed.
@@ -301,16 +297,6 @@ Section GenericInstances.
    contravariant in the first argument, covariant in the second. *)
   
   Global Program 
-  Instance trans_contra_co_morphism
-    `(Transitive A R) : Proper (R --> R ++> impl) R.
-  
-  Next Obligation.
-  Proof with auto.
-    transitivity x...
-    transitivity x0...
-  Qed.
-
-  Global Program 
   Instance trans_contra_co_type_morphism
     `(Transitive A R) : Proper (R --> R ++> arrow) R.
   
@@ -323,15 +309,6 @@ Section GenericInstances.
   (** Proper declarations for partial applications. *)
 
   Global Program 
-  Instance trans_contra_inv_impl_morphism
-  `(Transitive A R) : Proper (R --> flip impl) (R x) | 3.
-
-  Next Obligation.
-  Proof with auto.
-    transitivity y...
-  Qed.
-
-  Global Program 
   Instance trans_contra_inv_impl_type_morphism
   `(Transitive A R) : Proper (R --> flip arrow) (R x) | 3.
 
@@ -380,15 +357,6 @@ Section GenericInstances.
   (** Every Transitive crelation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof to get an [R y z] goal. *)
 
   Global Program 
-  Instance trans_co_eq_inv_impl_morphism
-  `(Transitive A R) : Proper (R ==> (@eq A) ==> flip impl) R | 2.
-
-  Next Obligation.
-  Proof with auto.
-    transitivity y...
-  Qed.
-
-  Global Program 
   Instance trans_co_eq_inv_arrow_morphism
   `(Transitive A R) : Proper (R ==> (@eq A) ==> flip arrow) R | 2.
 
@@ -669,17 +637,6 @@ Qed.
 
 (** A [PartialOrder] is compatible with its underlying equivalence. *)
 Require Import Relation_Definitions.
-Instance PartialOrder_proper `(PartialOrder A eqA (R : crelation A)) :
-  Proper (eqA==>eqA==>iff) R.
-Proof.
-intros.
-apply proper_sym_impl_iff_2; auto with *.
-intros x x' Hx y y' Hy Hr.
-transitivity x.
-generalize (partial_order_equivalence x x'); compute; intuition.
-transitivity y; auto.
-generalize (partial_order_equivalence y y'); compute; intuition.
-Qed.
 
 Instance PartialOrder_proper_type `(PartialOrder A eqA R) :
   Proper (eqA==>eqA==>iffT) R.