aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2017-04-02 10:33:02 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2017-04-02 10:33:44 +0200
commitc68dc1748febb49f8eae7fc06794aa262c95a382 (patch)
tree2006f8da8d1fe022ab050decc4114ed5e4b1151a
parent58bc387700d1fe4856571e8fae5c1761f89adc38 (diff)
Fix documentation typo (bug #5433).
-rw-r--r--theories/Reals/Rsqrt_def.v2
1 files changed, 1 insertions, 1 deletions
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.