Fix [subrelation] clauses that privileged the weakest. Better impl args

for [PartialOrder] typeclass.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11882 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 3 insertions, 2 deletions

diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 659289f88..b058f67ba 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -368,7 +368,7 @@ Proof. intro A. exact (@predicate_implication_preorder (cons A (cons A nil))). Q
    We give an equivalent definition, up-to an equivalence relation 
    on the carrier. *)
 
-Class PartialOrder A eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} :=
+Class PartialOrder {A} eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} :=
   partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (inverse R)).
 
 (** The equivalence proof is sufficient for proving that [R] must be a morphism 
@@ -377,7 +377,8 @@ Class PartialOrder A eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} :=
 
 Instance partial_order_antisym `(PartialOrder A eqA R) : ! Antisymmetric A eqA R.
 Proof with auto.
-  reduce_goal. pose proof partial_order_equivalence as poe. do 3 red in poe. 
+  reduce_goal. 
+  pose proof partial_order_equivalence as poe. do 3 red in poe. 
   apply <- poe. firstorder.
 Qed.