Renommage des variables dans les schémas d'induction

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

2 files changed, 6 insertions, 6 deletions

diff --git a/contrib/omega/Zpower.v b/contrib/omega/Zpower.v
index 9e90f63e6..824012d12 100644
--- a/contrib/omega/Zpower.v
+++ b/contrib/omega/Zpower.v
@@ -306,7 +306,7 @@ Elim (convert p); Simpl;
 | Intro n; Rewrite (two_power_nat_S n);
   Unfold 2 Zdiv_rest_aux;
   Elim (iter_nat n (Z*Z)*Z Zdiv_rest_aux ((x,`0`),`1`));
-  Destruct y; Intros; Apply f_equal with f:=[z:Z]`2*z`; Assumption ]. 
+  Destruct a; Intros; Apply f_equal with f:=[z:Z]`2*z`; Assumption ]. 
 Save.
 
 Lemma Zdiv_rest_correct2 :
@@ -368,12 +368,12 @@ Lemma  Zdiv_rest_correct :
 Intros x p.
 Generalize (Zdiv_rest_correct1 x p); Generalize (Zdiv_rest_correct2 x p).
 Elim  (iter_pos p (Z*Z)*Z Zdiv_rest_aux ((x,`0`),`1`)).
-Induction y.
+Induction a.
 Intros.
 Elim H; Intros H1 H2; Clear H.
 Rewrite -> H0 in H1; Rewrite -> H0 in H2;
 Elim H2; Intros;
-Apply Zdiv_rest_proof with q:=y0 r:=y1; Assumption.
+Apply Zdiv_rest_proof with q:=a0 r:=b; Assumption.
 Save.
 
 End power_div_with_rest.
diff --git a/contrib/ring/Ring_normalize.v b/contrib/ring/Ring_normalize.v
index 34cb485fd..2590dd72b 100644
--- a/contrib/ring/Ring_normalize.v
+++ b/contrib/ring/Ring_normalize.v
@@ -278,7 +278,7 @@ Variable vm : (varmap A).
  * choice *)
 Definition interp_var [i:index] := (varmap_find Azero i vm).
 
-Local ivl_aux := Fix ivl_aux {ivl_aux[x:index; t:varlist] : A := 
+(* Local *) Definition ivl_aux := Fix ivl_aux {ivl_aux[x:index; t:varlist] : A := 
   Cases t of
   | Nil_var => (interp_var x)
   | (Cons_var x' t') => (Amult (interp_var x) (ivl_aux x' t'))
@@ -290,14 +290,14 @@ Definition interp_vl :=  [l:varlist]
   | (Cons_var x t) => (ivl_aux x t)
   end.
 
-Local interp_m := [c:A][l:varlist] 
+(* Local *) Definition interp_m := [c:A][l:varlist] 
   Cases l of
   | Nil_var => c
   | (Cons_var x t) => 
       (Amult c (ivl_aux x t))
   end.
 
-Local ics_aux := Fix ics_aux{ics_aux[a:A; s:canonical_sum] : A :=  
+(* Local *) Definition ics_aux := Fix ics_aux{ics_aux[a:A; s:canonical_sum] : A :=  
   Cases s of
   | Nil_monom => a
   | (Cons_varlist l t) => (Aplus a (ics_aux (interp_vl l) t))