Solde de code mort et petites optimisations sur lesquels je suis

tombé au cours du temps


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

3 files changed, 24 insertions, 18 deletions

diff --git a/contrib/setoid_ring/InitialRing.v b/contrib/setoid_ring/InitialRing.v
index b7e9281d1..6542d280c 100644
--- a/contrib/setoid_ring/InitialRing.v
+++ b/contrib/setoid_ring/InitialRing.v
@@ -113,7 +113,7 @@ Section ZMORPHISM.
  Section ALMOST_RING.
  Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req.
    Add Morphism rsub : rsub_ext3. exact (ARsub_ext Rsth Reqe ARth). Qed.
-   Ltac norm := gen_srewrite 0 1 radd rmul rsub ropp req Rsth Reqe ARth.
+   Ltac norm := gen_srewrite Rsth Reqe ARth.
    Ltac add_push := gen_add_push radd Rsth Reqe ARth.
  
  Lemma same_gen : forall x, gen_phiPOS1 x == gen_phiPOS x.
@@ -161,7 +161,7 @@ Section ZMORPHISM.
  Variable Rth : ring_theory 0 1 radd rmul rsub ropp req.
  Let ARth := Rth_ARth Rsth Reqe Rth.
    Add Morphism rsub : rsub_ext4. exact (ARsub_ext Rsth Reqe ARth). Qed.
-   Ltac norm := gen_srewrite 0 1 radd rmul rsub ropp req Rsth Reqe ARth.
+   Ltac norm := gen_srewrite Rsth Reqe ARth.
    Ltac add_push := gen_add_push radd Rsth Reqe ARth.
   
 (*morphisms are extensionaly equal*)
@@ -317,8 +317,8 @@ Section NMORPHISM.
    Add Morphism rmul : rmul_ext4.  exact (Rmul_ext Reqe). Qed.
    Add Morphism ropp : ropp_ext4.  exact (Ropp_ext Reqe). Qed.
    Add Morphism rsub : rsub_ext5.  exact (ARsub_ext Rsth Reqe ARth). Qed.
-   Ltac norm := gen_srewrite 0 1 radd rmul rsub ropp req Rsth Reqe ARth.
-  
+   Ltac norm := gen_srewrite Rsth Reqe ARth.
+
  Definition gen_phiN1 x :=
   match x with
   | N0 => 0
@@ -433,7 +433,7 @@ Section NWORDMORPHISM.
 
  Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req.
    Add Morphism rsub : rsub_ext7. exact (ARsub_ext Rsth Reqe ARth). Qed.
-   Ltac norm := gen_srewrite 0 1 radd rmul rsub ropp req Rsth Reqe ARth.
+   Ltac norm := gen_srewrite Rsth Reqe ARth.
    Ltac add_push := gen_add_push radd Rsth Reqe ARth.
 
  Fixpoint gen_phiNword (w : Nword) : R :=
@@ -611,7 +611,7 @@ Section GEN_DIV.
   Add Morphism rmul : rmul_ext.  exact (Rmul_ext Reqe). Qed.
   Add Morphism ropp : ropp_ext.  exact (Ropp_ext Reqe). Qed.
   Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed.
- Ltac rsimpl := gen_srewrite 0 1 radd rmul rsub ropp req Rsth Reqe ARth.
+ Ltac rsimpl := gen_srewrite Rsth Reqe ARth.
 
  Definition triv_div x y :=  
    if ceqb x y then (cI, cO)
diff --git a/contrib/setoid_ring/Ring_polynom.v b/contrib/setoid_ring/Ring_polynom.v
index c62e64fdd..70199676c 100644
--- a/contrib/setoid_ring/Ring_polynom.v
+++ b/contrib/setoid_ring/Ring_polynom.v
@@ -66,7 +66,7 @@ Section MakeRingPol.
   Add Morphism rmul : rmul_ext.  exact (Rmul_ext Reqe). Qed.
   Add Morphism ropp : ropp_ext.  exact (Ropp_ext Reqe). Qed.
   Add Morphism rsub : rsub_ext. exact (ARsub_ext Rsth Reqe ARth). Qed.
- Ltac rsimpl := gen_srewrite 0 1 radd rmul rsub ropp req Rsth Reqe ARth.
+ Ltac rsimpl := gen_srewrite Rsth Reqe ARth.
  Ltac add_push := gen_add_push radd Rsth Reqe ARth.
  Ltac mul_push := gen_mul_push rmul Rsth Reqe ARth.
 
@@ -599,16 +599,22 @@ Section MakeRingPol.
  Ltac Esimpl :=
   repeat (progress (
    match goal with
-   | |- context [P0@?l] => rewrite (Pphi0 l)
-   | |- context [P1@?l] => rewrite (Pphi1 l)
-   | |- context [(mkPinj ?j ?P)@?l] => rewrite (mkPinj_ok j l P)
-   | |- context [(mkPX ?P ?i ?Q)@?l] => rewrite (mkPX_ok l P i Q)
-   | |- context [[cO]] => rewrite (morph0 CRmorph)
-   | |- context [[cI]] => rewrite (morph1 CRmorph)
-   | |- context [[?x +! ?y]] => rewrite ((morph_add CRmorph) x y)
-   | |- context [[?x *! ?y]] => rewrite ((morph_mul CRmorph) x y)
-   | |- context [[?x -! ?y]] => rewrite ((morph_sub CRmorph) x y)
-   | |- context [[-! ?x]] => rewrite ((morph_opp CRmorph) x)
+   | |- context [?P@?l] =>
+       match P with
+       | P0 => rewrite (Pphi0 l)
+       | P1 => rewrite (Pphi1 l)
+       | (mkPinj ?j ?P) => rewrite (mkPinj_ok j l P)
+       | (mkPX ?P ?i ?Q) => rewrite (mkPX_ok l P i Q)
+       end
+   | |- context [[?c]] =>
+       match c with
+       | cO => rewrite (morph0 CRmorph)
+       | cI => rewrite (morph1 CRmorph)
+       | ?x +! ?y => rewrite ((morph_add CRmorph) x y)
+       | ?x *! ?y => rewrite ((morph_mul CRmorph) x y)
+       | ?x -! ?y => rewrite ((morph_sub CRmorph) x y)
+       | -! ?x => rewrite ((morph_opp CRmorph) x)
+       end
    end));
   rsimpl; simpl. 
  
diff --git a/contrib/setoid_ring/Ring_theory.v b/contrib/setoid_ring/Ring_theory.v
index e993f6ba8..caa704595 100644
--- a/contrib/setoid_ring/Ring_theory.v
+++ b/contrib/setoid_ring/Ring_theory.v
@@ -572,7 +572,7 @@ End AddRing.
 (** Some simplification tactics*)
 Ltac gen_reflexivity Rsth := apply (Seq_refl _ _ Rsth).
 
-Ltac gen_srewrite O I add mul sub opp eq Rsth Reqe ARth :=
+Ltac gen_srewrite Rsth Reqe ARth :=
   repeat first
      [ gen_reflexivity Rsth
      | progress rewrite (ARopp_zero Rsth Reqe ARth)