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

28 files changed, 109 insertions, 37 deletions

diff --git a/plugins/micromega/Refl.v b/plugins/micromega/Refl.v
index 3b0de76b4..311748341 100644
--- a/plugins/micromega/Refl.v
+++ b/plugins/micromega/Refl.v
@@ -15,6 +15,7 @@
 
 Require Import List.
 Require Setoid.
+Import Morphisms Morphisms_Prop. (* For Hints *)
 
 Set Implicit Arguments.
 
diff --git a/plugins/micromega/Tauto.v b/plugins/micromega/Tauto.v
index b1d021768..fab676da8 100644
--- a/plugins/micromega/Tauto.v
+++ b/plugins/micromega/Tauto.v
@@ -15,6 +15,7 @@
 Require Import List.
 Require Import Refl.
 Require Import Bool.
+Import Morphisms Morphisms_Prop. (* For Hints *)
 
 Set Implicit Arguments.
 
diff --git a/plugins/ring/Setoid_ring_theory.v b/plugins/ring/Setoid_ring_theory.v
index 0444fe74a..a42c3ff72 100644
--- a/plugins/ring/Setoid_ring_theory.v
+++ b/plugins/ring/Setoid_ring_theory.v
@@ -8,6 +8,7 @@
 
 Require Export Bool.
 Require Export Setoid.
+Import Morphisms.
 
 Set Implicit Arguments.
 
diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index faa83dedc..dc47e9686 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
@@ -13,6 +13,7 @@ Require Import BinPos.
 Require Import BinNat.
 Require Import BinInt.
 Require Export Ring_theory.
+Import Morphisms. (* For Hints *)
 
 Open Local Scope positive_scope.
 Import RingSyntax.
diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v
index b3250a510..028804bb6 100644
--- a/plugins/setoid_ring/Ring_theory.v
+++ b/plugins/setoid_ring/Ring_theory.v
@@ -9,6 +9,7 @@
 Require Import Setoid.
 Require Import BinPos.
 Require Import BinNat.
+Import Morphisms. (* For Hints *)
 
 Set Implicit Arguments.
 
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 5c30f05aa..d57dd7b40 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -336,7 +336,18 @@ let class_params = function
 let add_class cl =
   add_new_class cl { cl_param = class_params cl }
 
-let load_coercion i (_,(coe,stre,isid,cls,clt,ps)) =
+let automatically_import_coercions = ref false
+
+open Goptions
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optname  = "automatic importation of coercions";
+      optkey   = ["Automatic";"Coercions";"Importation"];
+      optread  = (fun () -> !automatically_import_coercions);
+      optwrite = (:=) automatically_import_coercions }
+
+let cache_coercion (_,(coe,stre,isid,cls,clt,ps)) =
   add_class cls;
   add_class clt;
   let is,_ = class_info cls in
@@ -350,8 +361,17 @@ let load_coercion i (_,(coe,stre,isid,cls,clt,ps)) =
   add_new_coercion coe xf;
   add_coercion_in_graph (xf,is,it)
 
-let cache_coercion o =
-  load_coercion 1 o
+let load_coercion _ o =
+  if
+    !automatically_import_coercions || Flags.version_less_or_equal Flags.V8_2
+  then
+    cache_coercion o
+
+let open_coercion _ o =
+  if not 
+    (!automatically_import_coercions || Flags.version_less_or_equal Flags.V8_2)
+  then
+    cache_coercion o
 
 let subst_coercion (subst,(coe,stre,isid,cls,clt,ps as obj)) =
   let coe' = subst_coe_typ subst coe in
@@ -380,6 +400,7 @@ let classify_coercion (coe,stre,isid,cls,clt,ps as obj) =
 
 let (inCoercion,_) =
   declare_object {(default_object "COERCION") with
+    open_function = open_coercion;
     load_function = load_coercion;
     cache_function = cache_coercion;
     subst_function = subst_coercion;
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 0448b0b22..ba38f5458 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -402,12 +402,35 @@ type hint_action = | CreateDB of bool * transparent_state
 		   | AddTransparency of evaluable_global_reference list * bool
 		   | AddTactic of (global_reference option * pri_auto_tactic) list
 
+let automatically_import_hints = ref false
+
+open Goptions
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optname  = "automatic importation of hints";
+      optkey   = ["Automatic";"Hints";"Importation"];
+      optread  = (fun () -> !automatically_import_hints);
+      optwrite = (:=) automatically_import_hints }
+
 let cache_autohint (_,(local,name,hints)) =
   match hints with
   | CreateDB (b, st) -> searchtable_add (name, Hint_db.empty st b)
   | AddTransparency (grs, b) -> add_transparency name grs b
   | AddTactic hints -> add_hint name hints
 
+let load_autohint _ x =
+  if
+    !automatically_import_hints || Flags.version_less_or_equal Flags.V8_2
+  then
+    cache_autohint x
+
+let open_autohint _ x =
+  if
+    not (!automatically_import_hints || Flags.version_less_or_equal Flags.V8_2)
+  then
+    cache_autohint x
+
 let forward_subst_tactic =
   ref (fun _ -> failwith "subst_tactic is not installed for auto")
 
@@ -500,7 +523,8 @@ let discharge_autohint (_,(local,name,hintlist as obj)) =
 let (inAutoHint,_) =
   declare_object {(default_object "AUTOHINT") with
                     cache_function = cache_autohint;
-		    load_function = (fun _ -> cache_autohint);
+		    open_function = open_autohint;
+		    load_function = load_autohint;
 		    subst_function = subst_autohint;
 		    classify_function = classify_autohint }
 
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 :