aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/omega/Zpower.v6
-rw-r--r--contrib/ring/Ring_normalize.v6
-rw-r--r--theories/Logic/Eqdep_dec.v4
-rw-r--r--theories/Reals/Rbase.v12
-rw-r--r--theories/Reals/Rbasic_fun.v4
-rw-r--r--theories/Wellfounded/Disjoint_Union.v12
-rw-r--r--theories/Wellfounded/Lexicographic_Exponentiation.v4
-rw-r--r--theories/Wellfounded/Lexicographic_Product.v6
-rw-r--r--theories/Zarith/Zmisc.v4
9 files changed, 29 insertions, 29 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))
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index 54845ea07..6205fc603 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -71,7 +71,7 @@ Unfold nu.
Elim (eq_dec x y) using or_indd; Intros.
Reflexivity.
-Case y0; Trivial.
+Case b; Trivial.
Save.
@@ -123,7 +123,7 @@ Intro e.
Elim e using K_dec; Trivial.
Intros.
-Case y0; Trivial.
+Case b; Trivial.
Case H.
Reflexivity.
diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v
index 1fb31101d..91c3e5409 100644
--- a/theories/Reals/Rbase.v
+++ b/theories/Reals/Rbase.v
@@ -64,7 +64,7 @@ Hints Resolve imp_not_Req : real.
(**********)
Lemma Req_EM:(r1,r2:R)(r1==r2)\/``r1<>r2``.
Intros;Elim (total_order_T r1 r2);Intro.
-Case y; Auto with real.
+Case a; Auto with real.
Auto with real.
Save.
Hints Resolve Req_EM : real.
@@ -72,7 +72,7 @@ Hints Resolve Req_EM : real.
(**********)
Lemma total_order:(r1,r2:R)``r1<r2``\/(r1==r2)\/``r1>r2``.
Intros;Elim (total_order_T r1 r2);Intro;Auto.
-Elim y;Intro;Auto.
+Elim a;Intro;Auto.
Save.
(**********)
@@ -199,16 +199,16 @@ Save.
(*s Decidability of the order *)
Lemma total_order_Rlt:(r1,r2:R)(sumboolT ``r1<r2`` ~(``r1<r2``)).
Intros;Elim (total_order_T r1 r2);Intros.
-Elim y;Intro.
+Elim a;Intro.
Left;Assumption.
-Right;Rewrite y0;Apply Rlt_antirefl.
-Right;Unfold Rgt in y;Apply Rlt_antisym;Assumption.
+Right;Rewrite b;Apply Rlt_antirefl.
+Right;Unfold Rgt in b;Apply Rlt_antisym;Assumption.
Save.
(**********)
Lemma total_order_Rle:(r1,r2:R)(sumboolT ``r1<=r2`` ~(``r1<=r2``)).
Intros;Elim (total_order_T r1 r2);Intros.
-Left;Unfold Rle;Elim y;Auto with real.
+Left;Unfold Rle;Elim a;Auto with real.
Right; Auto with real.
Save.
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index b7466eb87..6b2106630 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -75,8 +75,8 @@ Save.
(*********)
Lemma case_Rabsolu:(r:R)(sumboolT (Rlt r R0) (Rge r R0)).
Intro;Generalize (total_order_Rle R0 r);Intro;Elim X;Intro;Clear X.
-Right;Apply (Rle_sym1 R0 r y).
-Left;Fold (Rgt R0 r);Apply (not_Rle R0 r y).
+Right;Apply (Rle_sym1 R0 r a).
+Left;Fold (Rgt R0 r);Apply (not_Rle R0 r b).
Save.
(*********)
diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v
index 162a31e83..d29262427 100644
--- a/theories/Wellfounded/Disjoint_Union.v
+++ b/theories/Wellfounded/Disjoint_Union.v
@@ -42,13 +42,13 @@ Proof.
Intros.
Unfold well_founded .
Induction a.
- Intro.
- Apply (acc_A_sum y).
- Apply (H y).
+ Intro a0.
+ Apply (acc_A_sum a0).
+ Apply (H a0).
- Intro.
- Apply (acc_B_sum H y).
- Apply (H0 y).
+ Intro b.
+ Apply (acc_B_sum H b).
+ Apply (H0 b).
Qed.
End Wf_Disjoint_Union.
diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v
index 06a9c123d..7b78ddb9c 100644
--- a/theories/Wellfounded/Lexicographic_Exponentiation.v
+++ b/theories/Wellfounded/Lexicographic_Exponentiation.v
@@ -301,7 +301,7 @@ Theorem wf_lex_exp :
(well_founded A leA)->(well_founded Power Lex_Exp).
Proof.
Unfold 2 well_founded .
- Induction a;Intros.
+ Induction a;Intros x y.
Apply Acc_intro.
Induction y0.
Unfold 1 lex_exp ;Simpl.
@@ -350,7 +350,7 @@ Proof.
Apply Acc_intro.
Induction y2.
Unfold 1 lex_exp .
- Simpl;Intros.
+ Simpl;Intros x4 y3. Intros.
Apply (H0 x4 y3);Auto with sets.
Intros.
diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v
index 157265047..a6da918e3 100644
--- a/theories/Wellfounded/Lexicographic_Product.v
+++ b/theories/Wellfounded/Lexicographic_Product.v
@@ -29,11 +29,11 @@ Lemma acc_A_B_lexprod : (x:A)(Acc A leA x)
->(y:(B x))(Acc (B x) (leB x) y)
->(Acc (sigS A B) LexProd (existS A B x y)).
Proof.
- Induction 1.
- Induction 4;Intros.
+ Induction 1; Intros x0 H0 H1 H2 y.
+ Induction 1;Intros.
Apply Acc_intro.
Induction y0.
- Intros.
+ Intros x2 y1 H6.
Simple Inversion H6;Intros.
Cut (leA x2 x0);Intros.
Apply H1;Auto with sets.
diff --git a/theories/Zarith/Zmisc.v b/theories/Zarith/Zmisc.v
index 2aa69092a..bc90b0612 100644
--- a/theories/Zarith/Zmisc.v
+++ b/theories/Zarith/Zmisc.v
@@ -303,8 +303,8 @@ Lemma Z_modulo_2 : (x:Z) `x >= 0` -> { y:Z | `x=2*y` }+{ y:Z | `x=2*y+1` }.
Proof.
Intros x Hx.
Elim (Zeven_odd_dec x); Intro.
-Left. Split with (Zdiv2 x). Exact (Zeven_div2 x y).
-Right. Split with (Zdiv2 x). Exact (Zodd_div2 x Hx y).
+Left. Split with (Zdiv2 x). Exact (Zeven_div2 x a).
+Right. Split with (Zdiv2 x). Exact (Zodd_div2 x Hx b).
Save.
(* Very simple *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 19:08:04 +0000