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, 23 insertions, 9 deletions

diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index bc05c252c..341c0e6f5 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -84,15 +84,29 @@ Qed.
 Let eq_trans := Setoid.Seq_trans _ _ Rsth.
 Let eq_sym := Setoid.Seq_sym _ _ Rsth.
 Let eq_refl := Setoid.Seq_refl _ _ Rsth.
-
-Hint Resolve eq_refl rdiv_def rinv_l rI_neq_rO CRmorph.(morph1) .
-Hint Resolve (Rmul_ext Reqe) (Rmul_ext Reqe) (Radd_ext Reqe)
-             (ARsub_ext Rsth Reqe ARth) (Ropp_ext Reqe) SRinv_ext.
-Hint Resolve (ARadd_0_l  ARth) (ARadd_comm  ARth) (ARadd_assoc ARth)
-             (ARmul_1_l  ARth) (ARmul_0_l  ARth)
-             (ARmul_comm  ARth) (ARmul_assoc ARth) (ARdistr_l  ARth)
-             (ARopp_mul_l ARth) (ARopp_add  ARth)
-             (ARsub_def  ARth) .
+Let mor1h := CRmorph.(morph1).
+
+Hint Resolve eq_refl rdiv_def rinv_l rI_neq_rO .
+
+Let lem1 := Rmul_ext Reqe.
+Let lem2 := Rmul_ext Reqe.
+Let lem3 := (Radd_ext Reqe).
+Let lem4 := ARsub_ext Rsth Reqe ARth.
+Let lem5 := Ropp_ext Reqe.
+Let lem6 := ARadd_0_l  ARth.
+Let lem7 := ARadd_comm  ARth.
+Let lem8 := (ARadd_assoc ARth).
+Let lem9 := ARmul_1_l  ARth.
+Let lem10 := (ARmul_0_l  ARth).
+Let lem11 := ARmul_comm  ARth.
+Let lem12 := ARmul_assoc ARth.
+Let lem13 := (ARdistr_l  ARth).
+Let lem14 := ARopp_mul_l ARth.
+Let lem15 := (ARopp_add  ARth).
+Let lem16 := ARsub_def  ARth.
+
+Hint Resolve lem1 lem2 lem3 lem4 lem5 lem6 lem7 lem8 lem9 lem10
+     lem11 lem12 lem13 lem14 lem15 lem16 SRinv_ext.
 
  (* Power coefficients *)
  Variable Cpow : Type.