aboutsummaryrefslogtreecommitdiff
path: root/doc/faq
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2017-02-14 18:01:48 +0100
committerPierre-Marie Pédrot2017-02-14 18:21:25 +0100
commit3234a893a1b3cfd6b51f1c26cc10e9690d8a703e (patch)
tree45fdbfc2fd03e30105d1ead1e184bdf6ef822de8 /doc/faq
parentcca57bcd89770e76e1bcc21eb41756dca2c51425 (diff)
parent4fd59386e7f60d16bfe9858c372b354d422ac0b6 (diff)
Merge branch 'master'.
Diffstat (limited to 'doc/faq')
-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?}