From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 28 Apr 2006 14:59:16 +0000
Subject: Imported Upstream version 8.0pl3+8.1alpha

---
 theories/Reals/Alembert.v | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

(limited to 'theories/Reals/Alembert.v')

diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v
index a691b189..e6bc69b6 100644
--- a/theories/Reals/Alembert.v
+++ b/theories/Reals/Alembert.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
  
-(*i $Id: Alembert.v,v 1.14.2.1 2004/07/16 19:31:10 herbelin Exp $ i*)
+(*i $Id: Alembert.v 8670 2006-03-28 22:16:14Z herbelin $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -30,7 +30,7 @@ intros An H H0.
 cut
  (sigT (fun l:R => is_lub (EUn (fun N:nat => sum_f_R0 An N)) l) ->
   sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l)).
-intro; apply X.
+intro X; apply X.
 apply completeness.
 unfold Un_cv in H0; unfold bound in |- *; cut (0 < / 2);
  [ intro | apply Rinv_0_lt_compat; prove_sup0 ].
@@ -107,7 +107,7 @@ red in |- *; intro; assert (H8 := H n); rewrite H7 in H8;
 replace (S x + 0)%nat with (S x); [ reflexivity | ring ].
 symmetry  in |- *; apply tech2; assumption.
 exists (sum_f_R0 An 0); unfold EUn in |- *; exists 0%nat; reflexivity.
-intro; elim X; intros.
+intro X; elim X; intros.
 apply existT with x; apply tech10;
  [ unfold Un_growing in |- *; intro; rewrite tech5;
     pattern (sum_f_R0 An n) at 1 in |- *; rewrite <- Rplus_0_r;
@@ -418,7 +418,7 @@ intros An k Hyp H H0.
 cut
  (sigT (fun l:R => is_lub (EUn (fun N:nat => sum_f_R0 An N)) l) ->
   sigT (fun l:R => Un_cv (fun N:nat => sum_f_R0 An N) l)).
-intro; apply X.
+intro X; apply X.
 apply completeness.
 assert (H1 := tech13 _ _ Hyp H0).
 elim H1; intros.
@@ -517,7 +517,7 @@ rewrite H10 in H11; elim (Rlt_irrefl _ H11).
 replace (S x0 + 0)%nat with (S x0); [ reflexivity | ring ].
 symmetry  in |- *; apply tech2; assumption.
 exists (sum_f_R0 An 0); unfold EUn in |- *; exists 0%nat; reflexivity.
-intro; elim X; intros.
+intro X; elim X; intros.
 apply existT with x; apply tech10;
  [ unfold Un_growing in |- *; intro; rewrite tech5;
     pattern (sum_f_R0 An n) at 1 in |- *; rewrite <- Rplus_0_r;
@@ -559,11 +559,11 @@ rewrite <- Rabs_mult.
 rewrite Rabs_Rabsolu.
 unfold Rdiv in H3; apply H3; assumption.
 apply H0.
-intro.
+intro X.
 elim X; intros.
 apply existT with x.
 assumption.
-intro.
+intro X.
 elim X; intros.
 apply existT with x.
 assumption.
@@ -581,7 +581,7 @@ intros.
 cut
  (sigT
     (fun l:R => Un_cv (fun N:nat => sum_f_R0 (fun i:nat => An i * x ^ i) N) l)).
-intro.
+intro X.
 elim X; intros.
 apply existT with x0.
 apply tech12; assumption.
@@ -723,4 +723,4 @@ unfold Rdiv in |- *; apply Rmult_lt_0_compat.
 assumption.
 apply Rinv_0_lt_compat; apply Rabs_pos_lt.
 red in |- *; intro H7; rewrite H7 in r; elim (Rlt_irrefl _ r).
-Qed.
\ No newline at end of file
+Qed.
-- 
cgit v1.2.3