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

1 files changed, 11 insertions, 7 deletions

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.