aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rwxr-xr-xdoc/RefMan-pre.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/RefMan-pre.tex b/doc/RefMan-pre.tex
index 36a10f664..1cbb18d4f 100755
--- a/doc/RefMan-pre.tex
+++ b/doc/RefMan-pre.tex
@@ -463,7 +463,7 @@ with {\Coq} makes interactive developments more friendly. All
mathematical Unicode symbols are usable within \CoqIde{}.
Finally, the module system of {\Coq} completes the picture of {\Coq}
-version 8.0. Tough released with an experimental status in the previous
+version 8.0. Though released with an experimental status in the previous
version 7.4, it should be considered as a salient feature of the new
version.