From cf3d8a16556e102b21521bf1b57dc2e43bf06951 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 21 Dec 2001 19:03:58 +0000
Subject: Passage coqweb

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

diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v
index c6596c5883..1dfa67c8db 100644
--- a/theories/Reals/R_sqr.v
+++ b/theories/Reals/R_sqr.v
@@ -245,7 +245,7 @@ Intros a b c d; Apply Rsqr_incr_0_var; [Rewrite Rsqr_times; Repeat Rewrite Rsqr_
 Save.
 
 (************************************************************)
-(* Resolution of a*X^2+b*X+c=0                              *)
+(* Resolution of [a*X^2+b*X+c=0]                            *)
 (************************************************************)
 
 Definition Delta [a:nonzeroreal;b,c:R] : R := ``(Rsqr b)-4*a*c``.
@@ -311,4 +311,4 @@ Symmetry; Apply Rmult_1l.
 Apply (cond_nonzero a).
 Unfold Rdiv; Field; Case a; Intros y H3; Apply prod_neq_R0; [DiscrR | Assumption].
 Unfold Delta; Reflexivity.
-Save.
\ No newline at end of file
+Save.
-- 
cgit v1.2.3