From bed9deeabad5e0935d55a37c0f2911d4d81ce84a Mon Sep 17 00:00:00 2001
From: desmettr
Date: Wed, 3 Jul 2002 18:26:47 +0000
Subject: *** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2836 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Reals/Rtrigo.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v
index 4a614bbf84..70452fbe00 100644
--- a/theories/Reals/Rtrigo.v
+++ b/theories/Reals/Rtrigo.v
@@ -25,7 +25,7 @@ Intros; Rewrite <- Ropp_mul1; Ring.
 Qed.
 
 (* Here, we have the euclidian division *)
-(* This lemma is used in the proof of sin_eq_0 : (sin x)=0<->x=2kPI *)
+(* This lemma is used in the proof of sin_eq_0 : (sin x)=0<->x=kPI *)
 Lemma euclidian_division : (x,y:R) ``y<>0`` -> (EXT k:Z | (EXT r : R | ``x==(IZR k)*y+r``/\``0<=r<(Rabsolu y)``)).
 Intros.
 Pose k0 := Cases (case_Rabsolu y) of
-- 
cgit v1.2.3