6 files changed, 32 insertions, 16 deletions
diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 0e820008ed..5abdecfc18 100755..100644
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -72,7 +72,8 @@
 %\newcommand{\spec}[1]{\{\,#1\,\}}
 
 % Building regular expressions
-\newcommand{\zeroone}[1]{\mbox{\sl [}#1\mbox{\sl ]}}
+\newcommand{\zeroone}[1]{\mbox{\sl [}{#1}\mbox{\sl ]}}
+\newcommand{\zeroonelax}[1]{\mbox{\sl [}#1\mbox{\sl ]}}
 %\newcommand{\zeroonemany}[1]{$\{$#1$\}$*}
 %\newcommand{\onemany}[1]{$\{$#1$\}$+}
 \newcommand{\nelistnosep}[1]{{#1} \mbox{\dots} {#1}}
@@ -97,8 +98,7 @@
 \newcommand{\camlpppp}{\textsc{Camlp4}}
 \newcommand{\emacs}{\textsc{GNU Emacs}}
 \newcommand{\ProofGeneral}{\textsc{Proof General}}
-\newcommand{\CIC}{\pCIC}
-\newcommand{\pCIC}{p\textsc{Cic}}
+\newcommand{\CIC}{\textsc{Cic}}
 \newcommand{\iCIC}{\textsc{Cic}}
 \newcommand{\FW}{\ensuremath{F_{\omega}}}
 \newcommand{\Program}{\textsc{Program}}
@@ -199,6 +199,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
@@ -258,13 +259,13 @@
 \newcommand{\forest}{\mbox{\textsf{forest}}}
 \newcommand{\from}{\mbox{\textsf{from}}}
 \newcommand{\hd}{\mbox{\textsf{hd}}}
-\newcommand{\Length}{\mbox{\textsf{Length}}}
+\newcommand{\haslength}{\mbox{\textsf{has\_length}}}
 \newcommand{\length}{\mbox{\textsf{length}}}
-\newcommand{\LengthA}{\mbox {\textsf{Length\_A}}}
-\newcommand{\List}{\mbox{\textsf{List}}}
-\newcommand{\ListA}{\mbox{\textsf{List\_A}}}
-\newcommand{\LNil}{\mbox{\textsf{Lnil}}}
-\newcommand{\LCons}{\mbox{\textsf{Lcons}}}
+\newcommand{\haslengthA}{\mbox {\textsf{has\_length~A}}}
+\newcommand{\List}{\mbox{\textsf{list}}}
+\newcommand{\ListA}{\mbox{\textsf{list}}~\ensuremath{A}}
+\newcommand{\nilhl}{\mbox{\textsf{nil\_hl}}}
+\newcommand{\conshl}{\mbox{\textsf{cons\_hl}}}
 \newcommand{\nat}{\mbox{\textsf{nat}}}
 \newcommand{\nO}{\mbox{\textsf{O}}}
 \newcommand{\nS}{\mbox{\textsf{S}}}
@@ -281,6 +282,13 @@
 \newcommand{\Type}{\mbox{\textsf{Type}}}
 \newcommand{\unfold}{\mbox{\textsf{unfold}}}
 \newcommand{\zeros}{\mbox{\textsf{zeros}}}
+\newcommand{\even}{\mbox{\textsf{even}}}
+\newcommand{\odd}{\mbox{\textsf{odd}}}
+\newcommand{\evenO}{\mbox{\textsf{even\_O}}}
+\newcommand{\evenS}{\mbox{\textsf{even\_S}}}
+\newcommand{\oddS}{\mbox{\textsf{odd\_S}}}
+\newcommand{\Prod}{\mbox{\textsf{prod}}}
+\newcommand{\Pair}{\mbox{\textsf{pair}}}
 
 %%%%%%%%%
 % Misc. %
@@ -364,6 +372,7 @@
 \newcommand{\myifthenelse}[3]{\kw{if} ~ #1 ~\kw{then} ~ #2 ~ \kw{else} ~ #3}
 \newcommand{\fun}[2]{\item[]{\tt {#1}}. \quad\\ #2}
 \newcommand{\WF}[2]{\ensuremath{{\cal W\!F}(#1)[#2]}}
+\newcommand{\WFTWOLINES}[2]{\ensuremath{{\cal W\!F}\begin{array}{l}(#1)\\\mbox{}[{#2}]\end{array}}}
 \newcommand{\WFE}[1]{\WF{E}{#1}}
 \newcommand{\WT}[4]{\ensuremath{#1[#2] \vdash #3 : #4}}
 \newcommand{\WTE}[3]{\WT{E}{#1}{#2}{#3}}
@@ -393,13 +402,13 @@
 \newcommand{\CIPI}[1]{\CIP{#1}{I}{P}}
 \newcommand{\CIF}[1]{\mbox{$\{#1\}_{f_1.. f_n}$}}
 %BEGIN LATEX
-\newcommand{\NInd}[3]{\mbox{{\sf Ind}$(#1)(\begin{array}[t]{@{}l}#2:=#3
+\newcommand{\NInd}[3]{\mbox{{\sf Ind}$(\begin{array}[t]{@{}l}#2:=#3
                                               \,)\end{array}$}}
-\newcommand{\Ind}[4]{\mbox{{\sf Ind}$(#1)[#2](\begin{array}[t]{@{}l@{}}#3:=#4
+\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}$}}
@@ -413,6 +422,7 @@
 \newcommand{\Fix}[2]{\mbox{\tt Fix}~#1\{#2\}}
 \newcommand{\CoFix}[2]{\mbox{\tt CoFix}~#1\{#2\}}
 \newcommand{\With}[2]{\mbox{\tt ~with~}}
+\newcommand{\letin}[3]{\kw{let}~#1:=#2~\kw{in}~#3}
 \newcommand{\subst}[3]{#1\{#2/#3\}}
 \newcommand{\substs}[4]{#1\{(#2/#3)_{#4}\}}
 \newcommand{\Sort}{\mbox{$\cal S$}}
diff --git a/doc/common/styles/html/coqremote/cover.html b/doc/common/styles/html/coqremote/cover.html
index 7b8f829601..1c415eca69 100644
--- a/doc/common/styles/html/coqremote/cover.html
+++ b/doc/common/styles/html/coqremote/cover.html
@@ -60,7 +60,8 @@
   <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>
+  <li>V8.6 © INRIA 2016</li>
 </ul>
 
 <p style="text-indent:0pt">This research was partly supported by IST
@@ -88,6 +89,7 @@
   <ul class="menu">
   <li><a href="general-index.html">General</a></li>
   <li><a href="command-index.html">Commands</a></li>
+  <li><a href="option-index.html">Options</a></li>
   <li><a href="tactic-index.html">Tactics</a></li>
   <li><a href="error-index.html">Errors</a></li>
   </ul>
diff --git a/doc/common/styles/html/coqremote/styles.hva b/doc/common/styles/html/coqremote/styles.hva
index 94fb0d38b1..a09dc4f85f 100644
--- a/doc/common/styles/html/coqremote/styles.hva
+++ b/doc/common/styles/html/coqremote/styles.hva
@@ -53,6 +53,7 @@
             <ul class="menu">
               <li><a href="general-index.html">General</a></li>
               <li><a href="command-index.html">Commands</a></li>
+              <li><a href="option-index.html">Options</a></li>
               <li><a href="tactic-index.html">Tactics</a></li>
               <li><a href="error-index.html">Errors</a></li>
             </ul>
diff --git a/doc/common/styles/html/simple/cover.html b/doc/common/styles/html/simple/cover.html
index c2ac2c19d8..25fb56320b 100644
--- a/doc/common/styles/html/simple/cover.html
+++ b/doc/common/styles/html/simple/cover.html
@@ -38,7 +38,8 @@
   <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>
+  <li>V8.6 © INRIA 2016</li>
 </ul>
 
 <p style="text-indent:0pt">This research was partly supported by IST
@@ -58,6 +59,7 @@
   <li><a href="toc.html">Table of contents</a></li>
   <li><a href="general-index.html">General index</a></li>
   <li><a href="command-index.html">Commands index</a></li>
+  <li><a href="option-index.html">Options index</a></li>
   <li><a href="tactic-index.html">Tactics index</a></li>
   <li><a href="error-index.html">Errors index</a></li>
 </ul>
diff --git a/doc/common/styles/html/simple/styles.hva b/doc/common/styles/html/simple/styles.hva
index 71c4ffedf0..20d0d4dd0a 100644
--- a/doc/common/styles/html/simple/styles.hva
+++ b/doc/common/styles/html/simple/styles.hva
@@ -32,6 +32,7 @@
   <li><a href="toc.html">Table of contents</a></li>
   <li><a href="general-index.html">General index</a></li>
   <li><a href="command-index.html">Commands index</a></li>
+  <li><a href="option-index.html">Options index</a></li>
   <li><a href="tactic-index.html">Tactics index</a></li>
   <li><a href="error-index.html">Errors index</a></li>
 </ul>
diff --git a/doc/common/title.tex b/doc/common/title.tex
index 4716c3156a..0e072b6b65 100755..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}