From 7465eba1019dc082f94b85aab5b7c28ae61c77ef Mon Sep 17 00:00:00 2001
From: notin
Date: Fri, 27 Oct 2006 13:05:29 +0000
Subject: Le caractère ² fait planter make doc

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

diff --git a/theories/Reals/Rprod.v b/theories/Reals/Rprod.v
index 758f7b357c..dbf236967e 100644
--- a/theories/Reals/Rprod.v
+++ b/theories/Reals/Rprod.v
@@ -98,7 +98,7 @@ Proof.
   ring.
 Qed. 
 
-(** We prove that (N!)²<=(2N-k)!*k! forall k in [|O;2N|] *)
+(** We prove that (N!)^2<=(2N-k)!*k! forall k in [|O;2N|] *)
 Lemma RfactN_fact2N_factk :
   forall N k:nat,
     (k <= 2 * N)%nat ->
-- 
cgit v1.2.3