Reverted 13293 commited mistakenly. Sorry for the noise.

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

5 files changed, 2 insertions, 11 deletions

diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v
index 3b7dea5e4..68f201897 100644
--- a/theories/Structures/GenericMinMax.v
+++ b/theories/Structures/GenericMinMax.v
@@ -7,7 +7,6 @@
 (***********************************************************************)
 
 Require Import Orders OrdersTac OrdersFacts Setoid Morphisms Basics.
-Import Morphisms_Prop. (* For Hints *)
 
 (** * A Generic construction of min and max *)
 
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index 5919a7646..6b9007fdd 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -7,7 +7,6 @@
 (***********************************************************************)
 
 Require Export SetoidList Morphisms OrdersTac.
-Import Morphisms_Prop. (* For Hints *)
 Set Implicit Arguments.
 Unset Strict Implicit.
 
diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v
index 01c6c62e7..f83e77ed8 100644
--- a/theories/Structures/Orders.v
+++ b/theories/Structures/Orders.v
@@ -7,8 +7,6 @@
 (***********************************************************************)
 
 Require Export Relations Morphisms Setoid Equalities.
-Import Morphisms_Prop. (* For Hints *)
-
 Set Implicit Arguments.
 Unset Strict Implicit.
 
diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v
index 69a7c3b9e..a28b79776 100644
--- a/theories/Structures/OrdersFacts.v
+++ b/theories/Structures/OrdersFacts.v
@@ -8,7 +8,6 @@
 
 Require Import Basics OrdersTac.
 Require Export Orders.
-Import Morphisms_Prop. (* For Hints *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -207,7 +206,6 @@ End OrderedTypeTest.
 
 Module OrderedTypeRev (O:OrderedTypeFull) <: OrderedTypeFull.
 
-Import O.
 Definition t := O.t.
 Definition eq := O.eq.
 Instance eq_equiv : Equivalence eq.
diff --git a/theories/Structures/OrdersTac.v b/theories/Structures/OrdersTac.v
index 80871d102..66a672c92 100644
--- a/theories/Structures/OrdersTac.v
+++ b/theories/Structures/OrdersTac.v
@@ -87,7 +87,6 @@ Ltac subst_eqns :=
 Definition interp_ord o :=
  match o with OEQ => O.eq | OLT => O.lt | OLE => O.le end.
 Local Notation "#" := interp_ord.
-Import Morphisms_Prop. (* For Hints *)
 
 Lemma trans : forall o o' x y z, #o x y -> #o' y z -> #(o+o') x z.
 Proof.
@@ -268,21 +267,19 @@ End OT_to_OrderTac.
 
 Module TotalOrderRev (O:TotalOrder) <: TotalOrder.
 
-Import O.
 Definition t := O.t.
 Definition eq := O.eq.
 Definition lt := flip O.lt.
 Definition le := flip O.le.
 Include EqLtLeNotation.
-Import RelationClasses. (* For hints *)
 
 (* No Instance syntax to avoid saturating the Equivalence tables *)
 Definition eq_equiv := O.eq_equiv.
 
 Instance lt_strorder: StrictOrder lt.
-Proof. unfold lt. auto using O.lt_strorder with *. Qed.
+Proof. unfold lt; auto with *. Qed.
 Instance lt_compat : Proper (eq==>eq==>iff) lt.
-Proof. unfold lt; auto using O.lt_compat with *. Qed.
+Proof. unfold lt; auto with *. Qed.
 
 Lemma le_lteq : forall x y, x<=y <-> x<y \/ x==y.
 Proof. intros; unfold le, lt, flip. rewrite O.le_lteq; intuition. Qed.