Tentative de suppression de l'import automatique des hints et coercions.

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

21 files changed, 55 insertions, 33 deletions

diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v
index c717e9bf5..e1ea24b91 100644
--- a/theories/Arith/Div2.v
+++ b/theories/Arith/Div2.v
@@ -6,10 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Lt.
-Require Import Plus.
-Require Import Compare_dec.
-Require Import Even.
+Require Import Lt Le Plus.
+Require Import Compare_dec Even.
 
 Open Local Scope nat_scope.
 
diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v
index b41d65c39..472af69c5 100644
--- a/theories/Bool/Bvector.v
+++ b/theories/Bool/Bvector.v
@@ -10,6 +10,7 @@
 
 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 f15ab222c..d6fc88338 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -13,11 +13,12 @@
  left projection. *)
 
 Require Import FMapInterface.
+Import Morphisms. (* For Hints *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Module Raw (X:OrderedType).
+Module Raw (Import X:OrderedType).
 
 Module Import MX := OrderedTypeFacts X.
 Module Import PX := KeyOrderedType X.
@@ -1154,7 +1155,7 @@ Section Elt.
 
 End Make.
 
-Module Make_ord (X: OrderedType)(D : OrderedType) <:
+Module Make_ord (X: OrderedType)(Import D : OrderedType) <:
 Sord with Module Data := D
         with Module MapS.E := X.
 
@@ -1332,6 +1333,7 @@ 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 6c1e8ca89..a952d5679 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -12,11 +12,12 @@
  [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 (X:DecidableType).
+Module Raw (Import X:DecidableType).
 
 Module Import PX := KeyDecidableType X.
 
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index d1e3f90b3..7df48dca0 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 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 88ccdb126..64f534f90 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -9,6 +9,7 @@
 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 ea53c7d06..23ca56524 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.v
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 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 4cc48af66..98d447824 100644
--- a/theories/NArith/Pminmax.v
+++ b/theories/NArith/Pminmax.v
@@ -7,6 +7,7 @@
 (************************************************************************)
 
 Require Import Orders BinPos Pnat POrderedType GenericMinMax.
+Import Plus. (* For Hints *)
 
 (** * Maximum and Minimum of two positive numbers *)
 
@@ -123,4 +124,4 @@ Proof.
  apply plus_min_distr_l.
 Qed.
 
-End P.
\ No newline at end of file
+End P.
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index 9f587a1d0..321c9eb89 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -9,6 +9,7 @@
 (************************************************************************)
 
 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 1f6c615bc..79c95ded6 100644
--- a/theories/Numbers/NatInt/NZDiv.v
+++ b/theories/Numbers/NatInt/NZDiv.v
@@ -9,6 +9,7 @@
 (** 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 acc43fc17..6aa09dd54 100644
--- a/theories/Numbers/NatInt/NZMulOrder.v
+++ b/theories/Numbers/NatInt/NZMulOrder.v
@@ -10,6 +10,7 @@
 
 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 bfbcc2c65..dc62b1717 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -9,6 +9,7 @@
 (************************************************************************)
 
 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 f26f56d0c..249674f3e 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -11,6 +11,7 @@
 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 5b7aa24b7..4cada985d 100644
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.v
@@ -68,7 +68,7 @@ Section multiset_defs.
   Qed.
 
 
-  Require Plus. (* comm. and ass. of plus *)
+  Require Import Plus. (* comm. and ass. of plus *)
 
   Lemma munion_comm : forall x y:multiset, meq (munion x y) (munion y x).
   Proof.
@@ -168,6 +168,8 @@ 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 68f201897..3b7dea5e4 100644
--- a/theories/Structures/GenericMinMax.v
+++ b/theories/Structures/GenericMinMax.v
@@ -7,6 +7,7 @@
 (***********************************************************************)
 
 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 6b9007fdd..5919a7646 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -7,6 +7,7 @@
 (***********************************************************************)
 
 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 f83e77ed8..01c6c62e7 100644
--- a/theories/Structures/Orders.v
+++ b/theories/Structures/Orders.v
@@ -7,6 +7,8 @@
 (***********************************************************************)
 
 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 a28b79776..69a7c3b9e 100644
--- a/theories/Structures/OrdersFacts.v
+++ b/theories/Structures/OrdersFacts.v
@@ -8,6 +8,7 @@
 
 Require Import Basics OrdersTac.
 Require Export Orders.
+Import Morphisms_Prop. (* For Hints *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -206,6 +207,7 @@ 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 66a672c92..80871d102 100644
--- a/theories/Structures/OrdersTac.v
+++ b/theories/Structures/OrdersTac.v
@@ -87,6 +87,7 @@ 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.
@@ -267,19 +268,21 @@ 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 with *. Qed.
+Proof. unfold lt. auto using O.lt_strorder with *. Qed.
 Instance lt_compat : Proper (eq==>eq==>iff) lt.
-Proof. unfold lt; auto with *. Qed.
+Proof. unfold lt; auto using O.lt_compat 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 2dce5fbe4..a8b5576f5 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 with arith.
-    intro. right. apply Znot_le_gt; auto with arith.
+    elim Z_le_dec; auto.
+    intro. right. apply Znot_le_gt; auto.
   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 with arith.
-    intro. right. apply Znot_ge_lt; auto with arith.
+    elim Z_ge_dec; auto.
+    intro. right. apply Znot_ge_lt; auto.
   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 with arith.
-    intro. left. elim (Zcompare_Eq_iff_eq x y); auto with arith.
-    intro H1. absurd (x > y); auto with arith.
+    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.
   Defined.
 
 End decidability.
diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v
index 4dfce35ce..0c87f6223 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 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.
+  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.
 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 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.
+  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.
 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 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.
+  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.
 Qed.
 
 Lemma Z_modulo_2 :