From 0919391f43729bf172ab00c8dec9438a0a9f59ab Mon Sep 17 00:00:00 2001 From: msozeau Date: Fri, 26 Oct 2012 01:29:33 +0000 Subject: 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 --- plugins/setoid_ring/Field_theory.v | 32 +++++++++++++++++++++++--------- 1 file changed, 23 insertions(+), 9 deletions(-) (limited to 'plugins/setoid_ring/Field_theory.v') 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. -- cgit v1.2.3