From 7da3cb6694b0584f8e01e8c75ca93ff63d8984f0 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Wed, 25 Apr 2001 07:56:54 +0000
Subject: coqweb

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1711 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Reals/Rseries.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v
index 2e94528d50..a388e2ae3b 100644
--- a/theories/Reals/Rseries.v
+++ b/theories/Reals/Rseries.v
@@ -12,7 +12,7 @@ Require Export Rderiv.
 Require Classical.
 Require Compare.
 
-(* classical is needed for Un_cv_crit *)
+(* classical is needed for [Un_cv_crit] *)
 (*********************************************************)
 (*           Definition of sequence and properties       *)
 (*                                                       *)
@@ -84,7 +84,7 @@ Unfold ge in H0;Generalize (H0 (S n0) H1 (lt_le_S n0 n1 y));Intro;
 Save.
 
 
-(* classical is needed: not_all_not_ex *)
+(* classical is needed: [not_all_not_ex] *)
 (*********)
 Lemma Un_cv_crit:Un_growing->(bound EUn)->(ExT [l:R] (Un_cv l)).
 Unfold Un_growing Un_cv;Intros;
-- 
cgit v1.2.3