From c68dc1748febb49f8eae7fc06794aa262c95a382 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Sun, 2 Apr 2017 10:33:02 +0200
Subject: Fix documentation typo (bug #5433).

---
 theories/Reals/Rsqrt_def.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'theories/Reals')

diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v
index b3c9c7449..6c2b0a1a7 100644
--- a/theories/Reals/Rsqrt_def.v
+++ b/theories/Reals/Rsqrt_def.v
@@ -648,7 +648,7 @@ Proof.
 Qed.
 
 (** We can now define the square root function as the reciprocal
-   transformation of the square root function *)
+   transformation of the square function *)
 Lemma Rsqrt_exists :
   forall y:R, 0 <= y -> { z:R | 0 <= z /\ y = Rsqr z }.
 Proof.
-- 
cgit v1.2.3