diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/common/styles/html/coqremote/cover.html | 1 | ||||
| -rw-r--r-- | doc/common/styles/html/simple/cover.html | 1 | ||||
| -rw-r--r-- | doc/faq/FAQ.tex | 4 | ||||
| -rw-r--r-- | doc/refman/Classes.tex | 1 |
4 files changed, 5 insertions, 2 deletions
diff --git a/doc/common/styles/html/coqremote/cover.html b/doc/common/styles/html/coqremote/cover.html index 6ec4dc1af0..1c415eca69 100644 --- a/doc/common/styles/html/coqremote/cover.html +++ b/doc/common/styles/html/coqremote/cover.html @@ -61,6 +61,7 @@ <li>V8.3 © INRIA 2010-2011</li> <li>V8.4 © INRIA 2012-2014</li> <li>V8.5 © INRIA 2015-2016</li> + <li>V8.6 © INRIA 2016</li> </ul> <p style="text-indent:0pt">This research was partly supported by IST diff --git a/doc/common/styles/html/simple/cover.html b/doc/common/styles/html/simple/cover.html index 328bd68daf..25fb56320b 100644 --- a/doc/common/styles/html/simple/cover.html +++ b/doc/common/styles/html/simple/cover.html @@ -39,6 +39,7 @@ <li>V8.3 © INRIA 2010-2011</li> <li>V8.4 © INRIA 2012-2014</li> <li>V8.5 © INRIA 2015-2016</li> + <li>V8.6 © INRIA 2016</li> </ul> <p style="text-indent:0pt">This research was partly supported by IST 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?} diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index bd8ee450ef..acfc4bea93 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -380,6 +380,7 @@ use implicit generalization (see \ref{SectionContext}). \asubsection{\tt typeclasses eauto} \tacindex{typeclasses eauto} +\label{typeclasseseauto} The {\tt typeclasses eauto} tactic uses a different resolution engine than {\tt eauto} and {\tt auto}. The main differences are the following: |