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

21 files changed, 33 insertions, 55 deletions

diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index e1ea24b91..c717e9bf5 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -6,8 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Lt Le Plus.
-Require Import Compare_dec Even.
+Require Import Lt.
+Require Import Plus.
+Require Import Compare_dec.
+Require Import Even.
 
 Open Local Scope nat_scope.
 
diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v
index 472af69c5..b41d65c39 100644
--- a/theories/Bool/Bvector.v
+++ b/theories/Bool/Bvector.v
@@ -10,7 +10,6 @@
 
 Require Export Bool Sumbool.
 Require Import Minus.
-Import Lt. (* For Hints *)
 
 Open Local Scope nat_scope.
 
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index d6fc88338..f15ab222c 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -13,12 +13,11 @@
  left projection. *)
 
 Require Import FMapInterface.
-Import Morphisms. (* For Hints *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Module Raw (Import X:OrderedType).
+Module Raw (X:OrderedType).
 
 Module Import MX := OrderedTypeFacts X.
 Module Import PX := KeyOrderedType X.
@@ -1155,7 +1154,7 @@ Section Elt.
 
 End Make.
 
-Module Make_ord (X: OrderedType)(Import D : OrderedType) <:
+Module Make_ord (X: OrderedType)(D : OrderedType) <:
 Sord with Module Data := D
         with Module MapS.E := X.
 
@@ -1333,7 +1332,6 @@ Proof.
   inversion_clear Hm2; auto.
  destruct (IHm1 Hm11 (Build_slist Hm22));
   [ apply LT | apply EQ | apply GT ]; cmp_solve.
-Show.
 Qed.
 
 End Make_ord.
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index a952d5679..6c1e8ca89 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -12,12 +12,11 @@
  [FMapInterface.WS] using lists of pairs, unordered but without redundancy. *)
 
 Require Import FMapInterface.
-Import Morphisms_Prop. (* For Hints *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Module Raw (Import X:DecidableType).
+Module Raw (X:DecidableType).
 
 Module Import PX := KeyDecidableType X.
 
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 7df48dca0..d1e3f90b3 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 Require Import Le Gt Minus Bool.
-Import Plus. (* For Hints *)
 
 Set Implicit Arguments.
 
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index 64f534f90..88ccdb126 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -9,7 +9,6 @@
 Require Export List.
 Require Export Sorting.
 Require Export Setoid Basics Morphisms.
-Import Morphisms_Prop. (* For Hints *)
 Set Implicit Arguments.
 Unset Strict Implicit.
 
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v
index 23ca56524..ea53c7d06 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.v
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 Require Import Bool Setoid Bvector BinPos BinNat.
-Import Le Morphisms. (* For Hints *)
 
 (** Operation over bits of a [N] number. *)
 
diff --git a/theories/NArith/Pminmax.v b/theories/NArith/Pminmax.v
index 98d447824..4cc48af66 100644
--- a/theories/NArith/Pminmax.v
+++ b/theories/NArith/Pminmax.v
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 Require Import Orders BinPos Pnat POrderedType GenericMinMax.
-Import Plus. (* For Hints *)
 
 (** * Maximum and Minimum of two positive numbers *)
 
@@ -124,4 +123,4 @@ Proof.
  apply plus_min_distr_l.
 Qed.
 
-End P.
+End P.
\ No newline at end of file
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index 321c9eb89..9f587a1d0 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 Require Import NZAxioms.
-Import Morphisms_Prop. (* For Hints *)
 
 Module Type NZBasePropSig (Import NZ : NZDomainSig').
 
diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v
index 79c95ded6..1f6c615bc 100644
--- a/theories/Numbers/NatInt/NZDiv.v
+++ b/theories/Numbers/NatInt/NZDiv.v
@@ -9,7 +9,6 @@
 (** Euclidean Division *)
 
 Require Import NZAxioms NZMulOrder.
-Import Morphisms_Prop. (* For Hints *)
 
 (** The first signatures will be common to all divisions over NZ, N and Z *)
 
diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v
index 6aa09dd54..acc43fc17 100644
--- a/theories/Numbers/NatInt/NZMulOrder.v
+++ b/theories/Numbers/NatInt/NZMulOrder.v
@@ -10,7 +10,6 @@
 
 Require Import NZAxioms.
 Require Import NZAddOrder.
-Import Morphisms_Prop. (* For Hints *)
 
 Module Type NZMulOrderPropSig (Import NZ : NZOrdAxiomsSig').
 Include NZAddOrderPropSig NZ.
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index dc62b1717..bfbcc2c65 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 Require Import NZAxioms NZBase Decidable OrdersTac.
-Import Morphisms_Prop. (* For Hints *)
 
 Module Type NZOrderPropSig
  (Import NZ : NZOrdSig')(Import NZBase : NZBasePropSig NZ).
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index 249674f3e..f26f56d0c 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -11,7 +11,6 @@
 Require Export Decidable.
 Require Export NAxioms.
 Require Import NZProperties.
-Import Morphisms_Prop. (* For Hints *)
 
 Module NBasePropFunct (Import N : NAxiomsSig').
 (** First, we import all known facts about both natural numbers and integers. *)
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v
index 4cada985d..5b7aa24b7 100644
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.v
@@ -68,7 +68,7 @@ Section multiset_defs.
   Qed.
 
 
-  Require Import Plus. (* comm. and ass. of plus *)
+  Require Plus. (* comm. and ass. of plus *)
 
   Lemma munion_comm : forall x y:multiset, meq (munion x y) (munion y x).
   Proof.
@@ -168,8 +168,6 @@ Section multiset_defs.
 
   (** SingletonBag *)
 
-Import Morphisms_Prop Morphisms. (* For Hints *)
-
   Lemma meq_singleton : forall a a',
     eqA a a' -> meq (SingletonBag a) (SingletonBag a').
   Proof.
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.
diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v
index a8b5576f5..2dce5fbe4 100644
--- a/theories/ZArith/ZArith_dec.v
+++ b/theories/ZArith/ZArith_dec.v
@@ -100,8 +100,8 @@ Section decidability.
 
   Definition Z_le_gt_dec : {x <= y} + {x > y}.
   Proof.
-    elim Z_le_dec; auto.
-    intro. right. apply Znot_le_gt; auto.
+    elim Z_le_dec; auto with arith.
+    intro. right. apply Znot_le_gt; auto with arith.
   Defined.
 
   Definition Z_gt_le_dec : {x > y} + {x <= y}.
@@ -111,17 +111,17 @@ Section decidability.
 
   Definition Z_ge_lt_dec : {x >= y} + {x < y}.
   Proof.
-    elim Z_ge_dec; auto.
-    intro. right. apply Znot_ge_lt; auto.
+    elim Z_ge_dec; auto with arith.
+    intro. right. apply Znot_ge_lt; auto with arith.
   Defined.
 
   Definition Z_le_lt_eq_dec : x <= y -> {x < y} + {x = y}.
   Proof.
     intro H.
     apply Zcompare_rec with (n := x) (m := y).
-    intro. right. elim (Zcompare_Eq_iff_eq x y); auto.
-    intro. left. elim (Zcompare_Eq_iff_eq x y); auto.
-    intro H1. absurd (x > y); auto.
+    intro. right. elim (Zcompare_Eq_iff_eq x y); auto with arith.
+    intro. left. elim (Zcompare_Eq_iff_eq x y); auto with arith.
+    intro H1. absurd (x > y); auto with arith.
   Defined.
 
 End decidability.
diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v
index 0c87f6223..4dfce35ce 100644
--- a/theories/ZArith/Zeven.v
+++ b/theories/ZArith/Zeven.v
@@ -145,32 +145,32 @@ Definition Zdiv2 (z:Z) :=
 Lemma Zeven_div2 : forall n:Z, Zeven n -> n = 2 * Zdiv2 n.
 Proof.
   intro x; destruct x.
-  auto.
-  destruct p; auto.
-  intros. absurd (Zeven (Zpos (xI p))); red in |- *; auto.
-  intros. absurd (Zeven 1); red in |- *; auto.
-  destruct p; auto.
-  intros. absurd (Zeven (Zneg (xI p))); red in |- *; auto.
-  intros. absurd (Zeven (-1)); red in |- *; auto.
+  auto with arith.
+  destruct p; auto with arith.
+  intros. absurd (Zeven (Zpos (xI p))); red in |- *; auto with arith.
+  intros. absurd (Zeven 1); red in |- *; auto with arith.
+  destruct p; auto with arith.
+  intros. absurd (Zeven (Zneg (xI p))); red in |- *; auto with arith.
+  intros. absurd (Zeven (-1)); red in |- *; auto with arith.
 Qed.
 
 Lemma Zodd_div2 : forall n:Z, n >= 0 -> Zodd n -> n = 2 * Zdiv2 n + 1.
 Proof.
   intro x; destruct x.
-  intros. absurd (Zodd 0); red in |- *; auto.
-  destruct p; auto.
-  intros. absurd (Zodd (Zpos (xO p))); red in |- *; auto.
-  intros. absurd (Zneg p >= 0); red in |- *; auto.
+  intros. absurd (Zodd 0); red in |- *; auto with arith.
+  destruct p; auto with arith.
+  intros. absurd (Zodd (Zpos (xO p))); red in |- *; auto with arith.
+  intros. absurd (Zneg p >= 0); red in |- *; auto with arith.
 Qed.
 
 Lemma Zodd_div2_neg :
   forall n:Z, n <= 0 -> Zodd n -> n = 2 * Zdiv2 n - 1.
 Proof.
   intro x; destruct x.
-  intros. absurd (Zodd 0); red in |- *; auto.
-  intros. absurd (Zneg p >= 0); red in |- *; auto.
-  destruct p; auto.
-  intros. absurd (Zodd (Zneg (xO p))); red in |- *; auto.
+  intros. absurd (Zodd 0); red in |- *; auto with arith.
+  intros. absurd (Zneg p >= 0); red in |- *; auto with arith.
+  destruct p; auto with arith.
+  intros. absurd (Zodd (Zneg (xO p))); red in |- *; auto with arith.
 Qed.
 
 Lemma Z_modulo_2 :