aboutsummaryrefslogtreecommitdiff
path: root/doc/faq/FAQ.tex
diff options
context:
space:
mode:
authorGuillaume Melquiond2016-11-24 15:14:19 +0100
committerGuillaume Melquiond2016-11-24 15:14:19 +0100
commita27ac0315dcbb99c64a260bac3988199a26b39cf (patch)
tree2cf20f9ee79494c190cbd0fb8658872dd785d30b /doc/faq/FAQ.tex
parentb16de62d20790930589795c3d10fbb07185ec22c (diff)
Fix some documentation typos.
Note: "dependant" does exist, but it is a noun and it means a person that is somehow financially dependent on someone else.
Diffstat (limited to 'doc/faq/FAQ.tex')
-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?}