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

7 files changed, 24 insertions, 33 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)
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 18a22e5c7..3406d06aa 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -151,9 +151,6 @@ let mk_clenv_from_n gls n (c,cty) =
 
 let mk_clenv_from gls = mk_clenv_from_n gls None
 
-let mk_clenv_rename_from gls (c,t) = 
-  mk_clenv_from gls (c,rename_bound_var (pf_env gls) [] t)
-
 let mk_clenv_rename_from_n gls n (c,t) = 
   mk_clenv_from_n gls n (c,rename_bound_var (pf_env gls) [] t)
 
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index e6cd960b2..1697bb3c2 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -53,9 +53,6 @@ val clenv_meta_type : clausenv -> metavariable -> types
 val mk_clenv_from : evar_info sigma -> constr * types -> clausenv
 val mk_clenv_from_n :
   evar_info sigma -> int option -> constr * types -> clausenv
-val mk_clenv_rename_from : evar_info sigma -> constr * types -> clausenv
-val mk_clenv_rename_from_n :
-  evar_info sigma -> int option -> constr * types -> clausenv
 val mk_clenv_type_of : evar_info sigma -> constr -> clausenv
 
 (***************************************************************)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 68cd19479..7fd7aabe4 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -217,14 +217,6 @@ let mutual_fix f n others gl =
 let mutual_cofix f others gl = 
   with_check (refiner (Prim (Cofix (f,others)))) gl
     
-let rename_bound_var_goal gls =
-  let { evar_hyps = sign; evar_concl = cl } = sig_it gls in 
-  let ids = ids_of_named_context (named_context_of_val sign) in
-  convert_concl_no_check 
-    (rename_bound_var (Global.env()) ids cl) DEFAULTcast gls 
-
-
-
 (* Versions with consistency checks *)
 
 let introduction id    = with_check (introduction_no_check id) 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index ed95ef285..6b6305a17 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -136,7 +136,6 @@ val rename_hyp_no_check       : (identifier*identifier) list -> tactic
 val mutual_fix      :
   identifier -> int -> (identifier * int * constr) list -> tactic
 val mutual_cofix    : identifier -> (identifier * constr) list -> tactic
-val rename_bound_var_goal : tactic
 
 (*s The most primitive tactics with consistency and type checking *)