3 files changed, 11 insertions, 11 deletions
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.