From 41bf87dd6a35255596638f1b1983a0b2d0d071b8 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 14 Feb 2001 15:57:26 +0000
Subject: Renommage des variables dans les schémas d'induction
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1387 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Wellfounded/Disjoint_Union.v               | 12 ++++++------
 theories/Wellfounded/Lexicographic_Exponentiation.v |  4 ++--
 theories/Wellfounded/Lexicographic_Product.v        |  6 +++---
 3 files changed, 11 insertions(+), 11 deletions(-)

(limited to 'theories/Wellfounded')

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.
-- 
cgit v1.2.3