4 files changed, 6 insertions, 5 deletions
diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 3b12f259b6..df5ee405f9 100644
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -198,6 +198,7 @@
 \newcommand{\pattern}{\nterm{pattern}} % pattern for pattern-matching
 \newcommand{\orpattern}{\nterm{or\_pattern}}
 \newcommand{\intropattern}{\nterm{intro\_pattern}}
+\newcommand{\intropatternlist}{\nterm{intro\_pattern\_list}}
 \newcommand{\disjconjintropattern}{\nterm{disj\_conj\_intro\_pattern}}
 \newcommand{\namingintropattern}{\nterm{naming\_intro\_pattern}}
 \newcommand{\termpattern}{\nterm{term\_pattern}} % term with holes
@@ -405,8 +406,8 @@
 \newcommand{\Ind}[4]{\mbox{{\sf Ind}$[#2](\begin{array}[t]{@{}l@{}}#3:=#4
                                                  \,)\end{array}$}}
 %END LATEX
-%HEVEA \newcommand{\NInd}[3]{\mbox{{\sf Ind}$(#1)(#2:=#3\,)$}}
-%HEVEA \newcommand{\Ind}[4]{\mbox{{\sf Ind}$(#1)[#2](#3:=#4\,)$}}
+%HEVEA \newcommand{\NInd}[3]{\mbox{{\sf Ind}$(#2\,:=\,#3)$}}
+%HEVEA \newcommand{\Ind}[4]{\mbox{{\sf Ind}$[#2](#3\,:=\,#4)$}}
 
 \newcommand{\Indp}[5]{\mbox{{\sf Ind}$_{#5}(#1)[#2](\begin{array}[t]{@{}l}#3:=#4
                                                  \,)\end{array}$}}
diff --git a/doc/common/styles/html/coqremote/cover.html b/doc/common/styles/html/coqremote/cover.html
index db82717094..6ec4dc1af0 100644
--- a/doc/common/styles/html/coqremote/cover.html
+++ b/doc/common/styles/html/coqremote/cover.html
@@ -60,7 +60,7 @@
   <li>V8.2 © INRIA 2008-2011</li>
   <li>V8.3 © INRIA 2010-2011</li>
   <li>V8.4 © INRIA 2012-2014</li>
-  <li>V8.5 © INRIA 2015</li>
+  <li>V8.5 © INRIA 2015-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 1641a1ed37..328bd68daf 100644
--- a/doc/common/styles/html/simple/cover.html
+++ b/doc/common/styles/html/simple/cover.html
@@ -38,7 +38,7 @@
   <li>V8.2 © INRIA 2008-2011</li>
   <li>V8.3 © INRIA 2010-2011</li>
   <li>V8.4 © INRIA 2012-2014</li>
-  <li>V8.5 © INRIA 2015</li>
+  <li>V8.5 © INRIA 2015-2016</li>
 </ul>
 
 <p style="text-indent:0pt">This research was partly supported by IST
diff --git a/doc/common/title.tex b/doc/common/title.tex
index 4716c3156a..0e072b6b65 100644
--- a/doc/common/title.tex
+++ b/doc/common/title.tex
@@ -45,7 +45,7 @@ V\coqversion, \today
 %END LATEX
 \copyright INRIA 1999-2004 ({\Coq} versions 7.x)
 
-\copyright INRIA 2004-2015 ({\Coq} versions 8.x)
+\copyright INRIA 2004-2016 ({\Coq} versions 8.x)
 
 #3
 \end{flushleft}