From a9cee971280fe8d1fb20d4208d71f7c399902c7d Mon Sep 17 00:00:00 2001
From: desmettr
Date: Wed, 22 Jan 2003 15:43:03 +0000
Subject: Commentaires

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

diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v
index 19e3d26023..35890cde81 100644
--- a/theories/Reals/R_sqrt.v
+++ b/theories/Reals/R_sqrt.v
@@ -12,7 +12,7 @@ Require Rbase.
 Require Rfunctions.
 Require Rsqrt_def.
 
-(* Voici un prolongement continu de Rsqrt sur R *)
+(* Here is a continuous extension of Rsqrt on R *)
 Definition sqrt : R->R := [x:R](Cases (case_Rabsolu x) of
       (leftT _) => R0
     | (rightT a) => (Rsqrt (mknonnegreal x (Rle_sym2 ? ? a))) end).
-- 
cgit v1.2.3