diff options
| author | Guillaume Melquiond | 2016-11-24 15:14:19 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2016-11-24 15:14:19 +0100 |
| commit | a27ac0315dcbb99c64a260bac3988199a26b39cf (patch) | |
| tree | 2cf20f9ee79494c190cbd0fb8658872dd785d30b /doc/faq/FAQ.tex | |
| parent | b16de62d20790930589795c3d10fbb07185ec22c (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.tex | 4 |
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?} |
