Change Hint Resolve, Immediate to take a global reference as argument

instead of a general constr: this is the most common case and does
not loose generality (one can simply define constrs before Hint Resolving
them). Benefits:
- Natural semantics for typeclasses, not class resolution needed at
Hint Resolve time, meaning less trouble for users as well.
- Ability to [Hint Remove] any hint so declared.
- Simplifies the implementation as well.


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

10 files changed, 67 insertions, 55 deletions

diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 36c328cf4..b8fdac8c9 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -56,7 +56,7 @@ Class Asymmetric {A} (R : relation A) :=
 Class Transitive {A} (R : relation A) :=
   transitivity : forall x y z, R x y -> R y z -> R x z.
 
-Hint Resolve @irreflexivity : ord.
+Hint Resolve irreflexivity : ord.
 
 Unset Implicit Arguments.
 
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 8c6fba508..3c0fc02e4 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -30,9 +30,10 @@ Require Import Logic.
 Open Scope nat_scope.
 
 Definition eq_S := f_equal S.
+Definition f_equal_nat := f_equal (A:=nat).
 
-Hint Resolve (f_equal S): v62.
-Hint Resolve (f_equal (A:=nat)): core.
+Hint Resolve eq_S: v62.
+Hint Resolve f_equal_nat: core.
 
 (** The predecessor function *)
 
@@ -40,7 +41,8 @@ Definition pred (n:nat) : nat := match n with
                                  | O => n
                                  | S u => u
                                  end.
-Hint Resolve (f_equal pred): v62.
+Definition f_equal_pred := f_equal pred.
+Hint Resolve f_equal_pred: v62.
 
 Theorem pred_Sn : forall n:nat, n = pred (S n).
 Proof.
@@ -88,8 +90,10 @@ Fixpoint plus (n m:nat) : nat :=
 
 where "n + m" := (plus n m) : nat_scope.
 
-Hint Resolve (f_equal2 plus): v62.
-Hint Resolve (f_equal2 (A1:=nat) (A2:=nat)): core.
+Definition f_equal2_plus := f_equal2 plus.
+Hint Resolve f_equal2_plus: v62.
+Definition f_equal2_nat := f_equal2 (A1:=nat) (A2:=nat). 
+Hint Resolve f_equal2_nat: core.
 
 Lemma plus_n_O : forall n:nat, n = n + 0.
 Proof.
@@ -127,8 +131,8 @@ Fixpoint mult (n m:nat) : nat :=
   end
 
 where "n * m" := (mult n m) : nat_scope.
-
-Hint Resolve (f_equal2 mult): core.
+Definition f_equal2_mult := f_equal2 mult.
+Hint Resolve f_equal2_mult: core.
 
 Lemma mult_n_O : forall n:nat, 0 = n * 0.
 Proof.
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index 7d3c383c1..8fd229917 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -101,10 +101,12 @@ Proof. split; induction 1; auto. Qed.
 (** Results concerning lists modulo [eqA] *)
 
 Hypothesis eqA_equiv : Equivalence eqA.
+Definition eqarefl := (@Equivalence_Reflexive _ _ eqA_equiv).
+Definition eqatrans := (@Equivalence_Transitive _ _ eqA_equiv).
+Definition eqasym := (@Equivalence_Symmetric _ _ eqA_equiv).
 
-Hint Resolve (@Equivalence_Reflexive _ _ eqA_equiv).
-Hint Resolve (@Equivalence_Transitive _ _ eqA_equiv).
-Hint Immediate (@Equivalence_Symmetric _ _ eqA_equiv).
+Hint Resolve eqarefl eqatrans.
+Hint Immediate eqasym.
 
 Ltac inv := invlist InA; invlist sort; invlist lelistA; invlist NoDupA.
 
@@ -633,7 +635,9 @@ Variable ltA : A -> A -> Prop.
 Hypothesis ltA_strorder : StrictOrder ltA.
 Hypothesis ltA_compat : Proper (eqA==>eqA==>iff) ltA.
 
-Hint Resolve (@StrictOrder_Transitive _ _ ltA_strorder).
+Let sotrans := (@StrictOrder_Transitive _ _ ltA_strorder).
+
+Hint Resolve sotrans.
 
 Notation InfA:=(lelistA ltA).
 Notation SortA:=(sort ltA).
@@ -821,7 +825,7 @@ Arguments eq {A} x _.
 Lemma filter_InA : forall f, Proper (eqA==>eq) f ->
  forall l x, InA x (List.filter f l) <-> InA x l /\ f x = true.
 Proof.
-clear ltA ltA_compat ltA_strorder.
+clear sotrans ltA ltA_strorder ltA_compat.
 intros; do 2 rewrite InA_alt; intuition.
 destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; exists y; intuition.
 destruct H0 as (y,(H0,H1)); rewrite filter_In in H1; intuition.
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index 1e66e2b5b..2182504dd 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -306,7 +306,7 @@ Include MSetGenTree.Props X I.
 Local Hint Immediate MX.eq_sym.
 Local Hint Unfold In lt_tree gt_tree Ok.
 Local Hint Constructors InT bst.
-Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans @ok.
+Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok.
 Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node.
 Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans.
 Local Hint Resolve elements_spec2.
diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v
index cacd91343..b7f3f96c9 100644
--- a/theories/MSets/MSetGenTree.v
+++ b/theories/MSets/MSetGenTree.v
@@ -341,7 +341,7 @@ Module Import MX := OrderedTypeFacts X.
 Scheme tree_ind := Induction for tree Sort Prop.
 Scheme bst_ind := Induction for bst Sort Prop.
 
-Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans @ok.
+Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok.
 Local Hint Immediate MX.eq_sym.
 Local Hint Unfold In lt_tree gt_tree.
 Local Hint Constructors InT bst.
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index d9b1fd9bb..b0e09b719 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -228,16 +228,14 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Notation Inf := (lelistA X.lt).
   Notation In := (InA X.eq).
 
-  (* TODO: modify proofs in order to avoid these hints *)
-  Hint Resolve (@Equivalence_Reflexive _ _ X.eq_equiv).
-  Hint Immediate (@Equivalence_Symmetric _ _ X.eq_equiv).
-  Hint Resolve (@Equivalence_Transitive _ _ X.eq_equiv).
+  Existing Instance X.eq_equiv.
+  Hint Extern 20 => solve [order].
 
   Definition IsOk s := Sort s.
 
   Class Ok (s:t) : Prop := ok : Sort s.
 
-  Hint Resolve @ok.
+  Hint Resolve ok.
   Hint Unfold Ok.
 
   Instance Sort_Ok s `(Hs : Sort s) : Ok s := { ok := Hs }.
@@ -343,7 +341,6 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   induction s; simpl; intros.
   intuition. inv; auto.
   elim_compare x a; inv; rewrite !InA_cons, ?IHs; intuition.
-  left; order.
   Qed.
 
   Lemma remove_inf :
@@ -402,8 +399,8 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Global Instance union_ok s s' : forall `(Ok s, Ok s'), Ok (union s s').
   Proof.
   repeat rewrite <- isok_iff; revert s s'.
-  induction2; constructors; try apply @ok; auto.
-  apply Inf_eq with x'; auto; apply union_inf; auto; apply Inf_eq with x; auto.
+  induction2; constructors; try apply @ok; auto. 
+  apply Inf_eq with x'; auto; apply union_inf; auto; apply Inf_eq with x; auto; order.
   change (Inf x' (union (x :: l) l')); auto.
   Qed.
 
@@ -412,7 +409,6 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
    In x (union s s') <-> In x s \/ In x s'.
   Proof.
   induction2; try rewrite ?InA_cons, ?Hrec, ?Hrec'; intuition; inv; auto.
-  left; order.
   Qed.
 
   Lemma inter_inf :
@@ -440,7 +436,6 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Proof.
   induction2; try rewrite ?InA_cons, ?Hrec, ?Hrec'; intuition; inv; auto;
    try sort_inf_in; try order.
-  left; order.
   Qed.
 
   Lemma diff_inf :
diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v
index b838495f9..92ad2fcfb 100644
--- a/theories/MSets/MSetRBT.v
+++ b/theories/MSets/MSetRBT.v
@@ -452,7 +452,7 @@ Local Notation Bk := (Node Black).
 Local Hint Immediate MX.eq_sym.
 Local Hint Unfold In lt_tree gt_tree Ok.
 Local Hint Constructors InT bst.
-Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans @ok.
+Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok.
 Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node.
 Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans.
 Local Hint Resolve elements_spec2.
diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v
index fd4114cd4..7c8c5e6de 100644
--- a/theories/MSets/MSetWeakList.v
+++ b/theories/MSets/MSetWeakList.v
@@ -118,16 +118,18 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
   Notation In := (InA X.eq).
 
   (* TODO: modify proofs in order to avoid these hints *)
-  Hint Resolve (@Equivalence_Reflexive _ _ X.eq_equiv).
-  Hint Immediate (@Equivalence_Symmetric _ _ X.eq_equiv).
-  Hint Resolve (@Equivalence_Transitive _ _ X.eq_equiv).
+  Let eqr:= (@Equivalence_Reflexive _ _ X.eq_equiv).
+  Let eqsym:= (@Equivalence_Symmetric _ _ X.eq_equiv).
+  Let eqtrans:= (@Equivalence_Transitive _ _ X.eq_equiv).
+  Hint Resolve eqr eqtrans.
+  Hint Immediate eqsym.
 
   Definition IsOk := NoDup.
 
   Class Ok (s:t) : Prop := ok : NoDup s.
 
   Hint Unfold Ok.
-  Hint Resolve @ok.
+  Hint Resolve ok.
 
   Instance NoDup_Ok s (nd : NoDup s) : Ok s := { ok := nd }.
 
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
index 94d3e97a5..809169a4d 100644
--- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
+++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v
@@ -354,6 +354,8 @@ Section Z_2nZ.
 
  (* Proof *)
  Context {specs : ZnZ.Specs ops}.
+ 
+ Create HintDb ZnZ.
 
  Hint Resolve
     ZnZ.spec_to_Z
@@ -397,9 +399,9 @@ Section Z_2nZ.
     ZnZ.spec_sqrt
     ZnZ.spec_WO
     ZnZ.spec_OW
-    ZnZ.spec_WW.
-
- Ltac wwauto := unfold ww_to_Z; auto.
+    ZnZ.spec_WW : ZnZ.
+ 
+ Ltac wwauto := unfold ww_to_Z; eauto with ZnZ.
 
  Let wwB := base _ww_digits.
 
@@ -414,7 +416,7 @@ Section Z_2nZ.
  Notation "[[ x ]]" := (zn2z_to_Z wwB to_Z x)  (at level 0, x at level 99).
 
  Let spec_ww_to_Z   : forall x, 0 <= [| x |] < wwB.
- Proof. refine (spec_ww_to_Z w_digits w_to_Z _);auto. Qed.
+ Proof. refine (spec_ww_to_Z w_digits w_to_Z _); wwauto. Qed.
 
  Let spec_ww_of_pos : forall p,
      Zpos p = (Z.of_N (fst (ww_of_pos p)))*wwB + [|(snd (ww_of_pos p))|].
@@ -438,15 +440,15 @@ Section Z_2nZ.
  Proof. reflexivity. Qed.
 
  Let spec_ww_1 : [|ww_1|] = 1.
- Proof. refine (spec_ww_1 w_0 w_1 w_digits w_to_Z _ _);auto. Qed.
+ Proof. refine (spec_ww_1 w_0 w_1 w_digits w_to_Z _ _);wwauto. Qed.
 
  Let spec_ww_Bm1 : [|ww_Bm1|] = wwB - 1.
- Proof. refine (spec_ww_Bm1 w_Bm1 w_digits w_to_Z _);auto. Qed.
+ Proof. refine (spec_ww_Bm1 w_Bm1 w_digits w_to_Z _);wwauto. Qed.
 
  Let spec_ww_compare :
   forall x y, compare x y = Z.compare [|x|] [|y|].
  Proof.
-  refine (spec_ww_compare w_0 w_digits w_to_Z w_compare _ _ _);auto.
+  refine (spec_ww_compare w_0 w_digits w_to_Z w_compare _ _ _);wwauto.
  Qed.
 
  Let spec_ww_eq0 : forall x, eq0 x = true -> [|x|] = 0.
@@ -455,14 +457,14 @@ Section Z_2nZ.
  Let spec_ww_opp_c : forall x, [-|opp_c x|] = -[|x|].
  Proof.
   refine(spec_ww_opp_c w_0 w_0 W0 w_opp_c w_opp_carry w_digits w_to_Z _ _ _ _);
-  auto.
+   wwauto.
  Qed.
 
  Let spec_ww_opp : forall x, [|opp x|] = (-[|x|]) mod wwB.
  Proof.
   refine(spec_ww_opp w_0 w_0 W0 w_opp_c w_opp_carry w_opp
    w_digits w_to_Z _ _ _ _ _);
-  auto.
+  wwauto.
  Qed.
 
  Let spec_ww_opp_carry : forall x, [|opp_carry x|] = wwB - [|x|] - 1.
@@ -473,7 +475,7 @@ Section Z_2nZ.
 
  Let spec_ww_succ_c : forall x, [+|succ_c x|] = [|x|] + 1.
  Proof.
-  refine (spec_ww_succ_c w_0 w_0 ww_1 w_succ_c w_digits w_to_Z _ _ _ _);auto.
+  refine (spec_ww_succ_c w_0 w_0 ww_1 w_succ_c w_digits w_to_Z _ _ _ _);wwauto.
  Qed.
 
  Let spec_ww_add_c  : forall x y, [+|add_c x y|] = [|x|] + [|y|].
@@ -495,7 +497,7 @@ Section Z_2nZ.
 
  Let spec_ww_add : forall x y, [|add x y|] = ([|x|] + [|y|]) mod wwB.
  Proof.
-  refine (spec_ww_add w_add_c w_add w_add_carry w_digits w_to_Z _ _ _ _);auto.
+  refine (spec_ww_add w_add_c w_add w_add_carry w_digits w_to_Z _ _ _ _);wwauto.
  Qed.
 
  Let spec_ww_add_carry : forall x y, [|add_carry x y|]=([|x|]+[|y|]+1)mod wwB.
@@ -608,13 +610,14 @@ Section Z_2nZ.
  Qed.
 
  Let spec_low: forall x,
-  w_to_Z (low x) = [|x|] mod wB.
+  w_to_Z (low x) = [|x|] mod wB. 
   intros x; case x; simpl low.
-    unfold ww_to_Z, w_to_Z, w_0; rewrite ZnZ.spec_0; simpl; auto.
+    unfold ww_to_Z, w_to_Z, w_0; rewrite ZnZ.spec_0; simpl; wwauto.
   intros xh xl; simpl.
   rewrite Z.add_comm; rewrite Z_mod_plus; auto with zarith.
   rewrite Zmod_small; auto with zarith.
-  unfold wB, base; auto with zarith.
+  unfold wB, base; eauto with ZnZ zarith.
+  unfold wB, base; eauto with ZnZ zarith.
  Qed.
 
  Let spec_ww_digits:
@@ -632,7 +635,7 @@ Section Z_2nZ.
  Proof.
  refine (spec_ww_head00 w_0 w_0W
                 w_compare w_head0 w_add2 w_zdigits _ww_zdigits
-                w_to_Z _ _ _ (eq_refl _ww_digits) _ _ _ _); auto.
+                w_to_Z _ _ _ (eq_refl _ww_digits) _ _ _ _); wwauto.
  exact ZnZ.spec_head00.
  exact ZnZ.spec_zdigits.
  Qed.
@@ -715,7 +718,7 @@ refine
       [|a|] = [|q|] * [|b|] + [|r|] /\
       0 <= [|r|] < [|b|].
  Proof.
-  refine (spec_ww_div w_digits ww_1 compare div_gt w_to_Z _ _ _ _);auto.
+  refine (spec_ww_div w_digits ww_1 compare div_gt w_to_Z _ _ _ _);wwauto.
  Qed.
 
  Let spec_ww_mod_gt : forall a b,
@@ -735,7 +738,7 @@ refine
 
  Let spec_ww_mod :  forall a b, 0 < [|b|] -> [|mod_ a b|] = [|a|] mod [|b|].
  Proof.
-  refine (spec_ww_mod w_digits W0 compare mod_gt w_to_Z _ _ _);auto.
+  refine (spec_ww_mod w_digits W0 compare mod_gt w_to_Z _ _ _);wwauto.
  Qed.
 
  Let spec_ww_gcd_gt : forall a b, [|a|] > [|b|] ->
@@ -743,7 +746,7 @@ refine
  Proof.
   refine (@spec_ww_gcd_gt t w_digits W0 w_to_Z _
     w_0 w_0 w_eq0 w_gcd_gt _ww_digits
-  _ gcd_gt_fix _ _ _ _ gcd_cont _);auto.
+  _ gcd_gt_fix _ _ _ _ gcd_cont _);wwauto.
   refine (@spec_ww_gcd_gt_aux t w_digits w_0 w_WW w_0W w_compare w_opp_c w_opp
    w_opp_carry w_sub_c w_sub w_sub_carry w_gcd_gt w_add_mul_div w_head0
    w_div21 div32 _ww_zdigits ww_1 add_mul_div w_zdigits w_to_Z
@@ -752,13 +755,13 @@ refine
   exact ZnZ.spec_zdigits.
   exact spec_ww_add_mul_div.
   refine (@spec_gcd_cont t w_digits ww_1 w_to_Z _ _ w_0 w_1 w_compare
-   _ _);auto.
+   _ _);wwauto.
  Qed.
 
  Let spec_ww_gcd : forall a b, Zis_gcd [|a|] [|b|] [|gcd a b|].
  Proof.
   refine (@spec_ww_gcd t w_digits W0 compare w_to_Z _ _ w_0 w_0 w_eq0 w_gcd_gt
-  _ww_digits _ gcd_gt_fix _ _ _ _ gcd_cont _);auto.
+  _ww_digits _ gcd_gt_fix _ _ _ _ gcd_cont _);wwauto.
   refine (@spec_ww_gcd_gt_aux t w_digits w_0 w_WW w_0W w_compare w_opp_c w_opp
    w_opp_carry w_sub_c w_sub w_sub_carry w_gcd_gt w_add_mul_div w_head0
    w_div21 div32 _ww_zdigits ww_1 add_mul_div w_zdigits w_to_Z
@@ -767,7 +770,7 @@ refine
   exact ZnZ.spec_zdigits.
   exact spec_ww_add_mul_div.
   refine (@spec_gcd_cont t w_digits ww_1 w_to_Z _ _ w_0 w_1 w_compare
-   _ _);auto.
+   _ _);wwauto.
  Qed.
 
  Let spec_ww_is_even : forall x,
@@ -818,6 +821,8 @@ refine
  Proof.
  unfold wB, base; apply Z.pow_pos_nonneg; auto with zarith.
  Qed.
+ 
+ Hint Transparent ww_to_Z.
 
  Let ww_testbit_high n x y : Z.pos w_digits <= n ->
   Z.testbit [|WW x y|] n =
@@ -826,8 +831,8 @@ refine
   intros Hn.
   assert (E : ZnZ.to_Z x = [|WW x y|] / wB).
   { simpl.
-    rewrite Z.div_add_l; auto with zarith.
-    now rewrite Z.div_small, Z.add_0_r. }
+    rewrite Z.div_add_l; eauto with ZnZ zarith.
+    now rewrite Z.div_small, Z.add_0_r; wwauto. }
   rewrite E.
   unfold wB, base. rewrite Z.div_pow2_bits.
   - f_equal; auto with zarith.
@@ -842,7 +847,7 @@ refine
   assert (E : ZnZ.to_Z y = [|WW x y|] mod wB).
   { simpl; symmetry.
     rewrite Z.add_comm, Z.mod_add; auto with zarith.
-    apply Z.mod_small; auto with zarith. }
+    apply Z.mod_small; eauto with ZnZ zarith. }
   rewrite E.
   unfold wB, base. symmetry. apply Z.mod_pow2_bits_low; auto.
  Qed.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 4dea8e07b..bfa975aab 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -409,7 +409,9 @@ Proof.
   rewrite Rplus_assoc; rewrite H; ring.
 Qed.
 
-Hint Resolve (f_equal (A:=R)): real.
+Definition f_equal_R := (f_equal (A:=R)).
+
+Hint Resolve f_equal_R : real.
 
 Lemma Rplus_eq_compat_l : forall r r1 r2, r1 = r2 -> r + r1 = r + r2.
 Proof.