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/Rsigma.v | 34 +++++++++++++++++-----------------
 1 file changed, 17 insertions(+), 17 deletions(-)

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

diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v
index 0027c274..76b44d96 100644
--- a/theories/Reals/Rsigma.v
+++ b/theories/Reals/Rsigma.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.
 
 Set Implicit Arguments.
 
@@ -28,8 +28,8 @@ Section Sigma.
   Proof.
     intros; induction  k as [| k Hreck].
     cut (low = 0%nat).
-    intro; rewrite H1; unfold sigma in |- *; rewrite <- minus_n_n;
-      rewrite <- minus_n_O; simpl in |- *; replace (high - 1)%nat with (pred high).
+    intro; rewrite H1; unfold sigma; rewrite <- minus_n_n;
+      rewrite <- minus_n_O; simpl; replace (high - 1)%nat with (pred high).
     apply (decomp_sum (fun k:nat => f k)).
     assumption.
     apply pred_of_minus.
@@ -42,8 +42,8 @@ Section Sigma.
     apply Hreck.
     assumption.
     apply lt_trans with (S k); [ apply lt_n_Sn | assumption ].
-    unfold sigma in |- *; replace (high - S (S k))%nat with (pred (high - S k)).
-    pattern (S k) at 3 in |- *; replace (S k) with (S k + 0)%nat;
+    unfold sigma; replace (high - S (S k))%nat with (pred (high - S k)).
+    pattern (S k) at 3; replace (S k) with (S k + 0)%nat;
       [ idtac | ring ].
     replace (sum_f_R0 (fun k0:nat => f (S (S k) + k0)) (pred (high - S k))) with
     (sum_f_R0 (fun k0:nat => f (S k + S k0)) (pred (high - S k))).
@@ -55,12 +55,12 @@ Section Sigma.
     replace (high - S (S k))%nat with (high - S k - 1)%nat.
     apply pred_of_minus.
     omega.
-    unfold sigma in |- *; replace (S k - low)%nat with (S (k - low)).
-    pattern (S k) at 1 in |- *; replace (S k) with (low + S (k - low))%nat.
-    symmetry  in |- *; apply (tech5 (fun i:nat => f (low + i))).
+    unfold sigma; replace (S k - low)%nat with (S (k - low)).
+    pattern (S k) at 1; replace (S k) with (low + S (k - low))%nat.
+    symmetry ; apply (tech5 (fun i:nat => f (low + i))).
     omega.
     omega.
-    rewrite <- H2; unfold sigma in |- *; rewrite <- minus_n_n; simpl in |- *;
+    rewrite <- H2; unfold sigma; rewrite <- minus_n_n; simpl;
       replace (high - S low)%nat with (pred (high - low)).
     replace (sum_f_R0 (fun k0:nat => f (S (low + k0))) (pred (high - low))) with
     (sum_f_R0 (fun k0:nat => f (low + S k0)) (pred (high - low))).
@@ -79,7 +79,7 @@ Section Sigma.
       (low <= k)%nat ->
       (k < high)%nat -> sigma low high - sigma low k = sigma (S k) high.
   Proof.
-    intros low high k H1 H2; symmetry  in |- *; rewrite (sigma_split H1 H2); ring.
+    intros low high k H1 H2; symmetry ; rewrite (sigma_split H1 H2); ring.
   Qed.
 
   Theorem sigma_diff_neg :
@@ -100,8 +100,8 @@ Section Sigma.
     apply sigma_split.
     apply le_n.
     assumption.
-    unfold sigma in |- *; rewrite <- minus_n_n.
-    simpl in |- *.
+    unfold sigma; rewrite <- minus_n_n.
+    simpl.
     replace (low + 0)%nat with low; [ reflexivity | ring ].
   Qed.
 
@@ -113,20 +113,20 @@ Section Sigma.
       generalize (lt_le_weak low high H1); intro H3;
         replace (f high) with (sigma high high).
     rewrite Rplus_comm; cut (high = S (pred high)).
-    intro; pattern high at 3 in |- *; rewrite H.
+    intro; pattern high at 3; rewrite H.
     apply sigma_split.
     apply le_S_n; rewrite <- H; apply lt_le_S; assumption.
     apply lt_pred_n_n; apply le_lt_trans with low; [ apply le_O_n | assumption ].
     apply S_pred with 0%nat; apply le_lt_trans with low;
       [ apply le_O_n | assumption ].
-    unfold sigma in |- *; rewrite <- minus_n_n; simpl in |- *;
+    unfold sigma; rewrite <- minus_n_n; simpl;
       replace (high + 0)%nat with high; [ reflexivity | ring ].
   Qed.
 
   Theorem sigma_eq_arg : forall low:nat, sigma low low = f low.
   Proof.
-    intro; unfold sigma in |- *; rewrite <- minus_n_n.
-    simpl in |- *; replace (low + 0)%nat with low; [ reflexivity | ring ].
+    intro; unfold sigma; rewrite <- minus_n_n.
+    simpl; replace (low + 0)%nat with low; [ reflexivity | ring ].
   Qed.
 
 End Sigma.
-- 
cgit v1.2.3