aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-10-26 01:29:33 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-10-26 01:29:33 +0000
commit0919391f43729bf172ab00c8dec9438a0a9f59ab (patch)
tree8afd08a9df68b58711da31a14bd2e8ec23b359ba /plugins
parent42bb029c878666a7a897ff615acdc60e7f67dd06 (diff)
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
Diffstat (limited to 'plugins')
-rw-r--r--plugins/setoid_ring/Field_theory.v32
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.