From d1f92d3bc420d0a5115a4533ca59b17f6b823515 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 4 Feb 2009 17:38:19 +0000
Subject: 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
---
 theories/Classes/Morphisms.v       | 6 +++---
 theories/Classes/RelationClasses.v | 5 +++--
 2 files changed, 6 insertions(+), 5 deletions(-)

diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 111d85f742..fa3684b74b 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -118,7 +118,7 @@ Proof. simpl_relation. apply subr. apply H. apply subl. apply H0. Qed.
 
 (** And of course it is reflexive. *)
 
-Instance morphisms_subrelation_refl : ! subrelation A R R | 10.
+Instance morphisms_subrelation_refl : ! subrelation A R R.
 Proof. simpl_relation. Qed.
 
 (** [Morphism] is itself a covariant morphism for [subrelation]. *)
@@ -151,10 +151,10 @@ Hint Extern 5 (@Morphism _ _ _) => subrelation_tac : typeclass_instances.
 
 (** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *)
 
-Instance iff_impl_subrelation : subrelation iff impl.
+Instance iff_impl_subrelation : subrelation iff impl | 2.
 Proof. firstorder. Qed.
 
-Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl).
+Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl) | 2.
 Proof. firstorder. Qed.
 
 Instance pointwise_subrelation {A} `(sub : subrelation B R R') :
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 659289f889..b058f67baa 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.
 
-- 
cgit v1.2.3