aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorGuillaume Melquiond2016-12-26 10:02:34 +0100
committerGuillaume Melquiond2016-12-26 10:11:41 +0100
commitdd710b9adbe7b27dccd6d4b21b90cb9bd07e5c07 (patch)
tree2953abfc518b395a67634f71ab483516e3324e8b /doc
parent827370fb97c138c16509bd549eaeddf94ca13c99 (diff)
Fix some documentation typos.
Diffstat (limited to 'doc')
-rw-r--r--doc/faq/FAQ.tex4
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index 48b61827d1..213fb03137 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -2587,8 +2587,8 @@ It is the language of commands of Gallina i.e. definitions, lemmas, {\ldots}
\Question{What is a dependent type?}
-A dependant type is a type which depends on some term. For instance
-``vector of size n'' is a dependant type representing all the vectors
+A dependent type is a type which depends on some term. For instance
+``vector of size n'' is a dependent type representing all the vectors
of size $n$. Its type depends on $n$
\Question{What is a proof by reflection?}