From e0d682ec25282a348d35c5b169abafec48555690 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Mon, 20 Aug 2012 18:27:01 +0200
Subject: Imported Upstream version 8.4dfsg

---
 theories/Reals/Cauchy_prod.v | 28 ++++++++++++++--------------
 1 file changed, 14 insertions(+), 14 deletions(-)

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

diff --git a/theories/Reals/Cauchy_prod.v b/theories/Reals/Cauchy_prod.v
index a9d5cde3..f6a48adc 100644
--- a/theories/Reals/Cauchy_prod.v
+++ b/theories/Reals/Cauchy_prod.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -10,7 +10,7 @@ Require Import Rbase.
 Require Import Rfunctions.
 Require Import Rseries.
 Require Import PartSum.
-Open Local Scope R_scope.
+Local Open Scope R_scope.
 
   (**********)
 Lemma sum_N_predN :
@@ -21,7 +21,7 @@ Proof.
   replace N with (S (pred N)).
   rewrite tech5.
   reflexivity.
-  symmetry  in |- *; apply S_pred with 0%nat; assumption.
+  symmetry ; apply S_pred with 0%nat; assumption.
 Qed.
 
   (**********)
@@ -51,7 +51,7 @@ Proof.
   elim (lt_irrefl _ H).
   cut (N = 0%nat \/ (0 < N)%nat).
   intro; elim H0; intro.
-  rewrite H1; simpl in |- *; ring.
+  rewrite H1; simpl; ring.
   replace (pred (S N)) with (S (pred N)).
   do 5 rewrite tech5.
   rewrite Rmult_plus_distr_r; rewrite Rmult_plus_distr_l; rewrite (HrecN H1).
@@ -66,7 +66,7 @@ Proof.
       repeat rewrite Rplus_assoc; apply Rplus_eq_compat_l.
   rewrite <- minus_n_n; cut (N = 1%nat \/ (2 <= N)%nat).
   intro; elim H2; intro.
-  rewrite H3; simpl in |- *; ring.
+  rewrite H3; simpl; ring.
   replace
     (sum_f_R0
       (fun k:nat =>
@@ -147,7 +147,7 @@ Proof.
       (pred (pred N))).
   repeat rewrite Rplus_assoc; apply Rplus_eq_compat_l.
   replace (pred (N - pred N)) with 0%nat.
-  simpl in |- *; rewrite <- minus_n_O.
+  simpl; rewrite <- minus_n_O.
   replace (S (pred N)) with N.
   replace (sum_f_R0 (fun k:nat => An (S N) * Bn (S k)) (pred (pred N))) with
     (sum_f_R0 (fun k:nat => Bn (S k) * An (S N)) (pred (pred N))).
@@ -161,11 +161,11 @@ Proof.
   apply S_pred with 0%nat; assumption.
   replace (N - pred N)%nat with 1%nat.
   reflexivity.
-  pattern N at 1 in |- *; replace N with (S (pred N)).
+  pattern N at 1; replace N with (S (pred N)).
   rewrite <- minus_Sn_m.
   rewrite <- minus_n_n; reflexivity.
   apply le_n.
-  symmetry  in |- *; apply S_pred with 0%nat; assumption.
+  symmetry ; apply S_pred with 0%nat; assumption.
   apply sum_eq; intros;
     rewrite
       (sum_N_predN (fun l:nat => An (S (S (l + i))) * Bn (N - l)%nat)
@@ -259,7 +259,7 @@ Proof.
   apply le_n.
   apply (fun p n m:nat => plus_le_reg_l n m p) with 1%nat.
   rewrite le_plus_minus_r.
-  simpl in |- *; assumption.
+  simpl; assumption.
   apply le_trans with 2%nat; [ apply le_n_Sn | assumption ].
   apply le_trans with 2%nat; [ apply le_n_Sn | assumption ].
   simpl; ring.
@@ -274,7 +274,7 @@ Proof.
   apply le_trans with (pred (pred N)).
   assumption.
   apply le_pred_n.
-  symmetry  in |- *; apply S_pred with 0%nat; assumption.
+  symmetry ; apply S_pred with 0%nat; assumption.
   apply INR_eq; rewrite S_INR; rewrite plus_INR; reflexivity.
   apply le_trans with (pred (pred N)).
   assumption.
@@ -427,7 +427,7 @@ Proof.
   apply le_trans with (pred (pred N)).
   assumption.
   apply le_pred_n.
-  symmetry  in |- *; apply S_pred with 0%nat; assumption.
+  symmetry ; apply S_pred with 0%nat; assumption.
   apply INR_eq; rewrite S_INR; rewrite plus_INR; simpl; ring.
   apply le_trans with (pred (pred N)).
   assumption.
@@ -441,11 +441,11 @@ Proof.
   inversion H1.
   left; reflexivity.
   right; apply le_n_S; assumption.
-  simpl in |- *.
+  simpl.
   replace (S (pred N)) with N.
   reflexivity.
   apply S_pred with 0%nat; assumption.
-  simpl in |- *.
+  simpl.
   cut ((N - pred N)%nat = 1%nat).
   intro; rewrite H2; reflexivity.
   rewrite pred_of_minus.
@@ -453,7 +453,7 @@ Proof.
   simpl; ring.
   apply lt_le_S; assumption.
   rewrite <- pred_of_minus; apply le_pred_n.
-  simpl in |- *; symmetry  in |- *; apply S_pred with 0%nat; assumption.
+  simpl; symmetry ; apply S_pred with 0%nat; assumption.
   inversion H.
   left; reflexivity.
   right; apply lt_le_trans with 1%nat; [ apply lt_n_Sn | exact H1 ].
-- 
cgit v1.2.3