Merge branch 'v8.5'

8 files changed, 43 insertions, 28 deletions

diff --git a/doc/common/styles/html/coqremote/cover.html b/doc/common/styles/html/coqremote/cover.html
index db8271709..6ec4dc1af 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 1641a1ed3..328bd68da 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 4716c3156..0e072b6b6 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}
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index f2ab79dce..51e881bff 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -2014,7 +2014,7 @@ variables, use
 
 Instead of letting the unification engine try to solve an existential variable
 by itself, one can also provide an explicit hole together with a tactic to solve
-it. Using the syntax {\tt \textdollar(\expr)\textdollar}, the user can put a
+it. Using the syntax {\tt ltac:(\expr)}, the user can put a
 tactic anywhere a term is expected. The order of resolution is not specified and
 is implementation-dependent. The inner tactic may use any variable defined in
 its scope, including repeated alternations between variables introduced by term
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex
index e0dc49666..cb2ab5dc2 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/refman/RefMan-pre.tex
@@ -1080,8 +1080,7 @@ Pierre-Marie Pédrot, Matthieu Sozeau, Arnaud Spiwack, Enrico Tassi as
 well as Bruno Barras, Yves Bertot, Frédéric Besson, Xavier Clerc,
 Pierre Corbineau, Jean-Christophe Filliâtre, Julien Forest, Sébastien
 Hinderer, Assia Mahboubi, Jean-Marc Notin, Yann Régis-Gianas, François
-Ripault, Carst Tankink. Maxime Dénès brilliantly coordinated the
-release process.
+Ripault, Carst Tankink. Maxime Dénès coordinated the release process.
 
 \begin{flushright}
 Paris, January 2015, revised December 2015,\\
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index ed1b79e56..c37367de5 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -407,6 +407,19 @@ Proof.
 
 \end{ErrMsgs}
 
+The bullet behavior can be controlled by the following commands.
+
+\begin{quote}
+Set Bullet Behavior "None".
+\end{quote}
+
+This makes bullets inactive.
+
+\begin{quote}
+Set Bullet Behavior "Strict Subproofs".
+\end{quote}
+
+This makes bullets active (this is the default behavior).
 
 \section{Requesting information}
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 36bd036a9..edf986392 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3026,23 +3026,33 @@ variables bound by a let-in construction inside the term itself (use
 here the {\tt zeta} flag). In any cases, opaque constants are not
 unfolded (see Section~\ref{Opaque}).
 
-The goal may be normalized with two strategies: {\em lazy} ({\tt lazy}
-tactic), or {\em call-by-value} ({\tt cbv} tactic). The lazy strategy
-is a call-by-need strategy, with sharing of reductions: the arguments of a
-function call are partially evaluated only when necessary, and if an
-argument is used several times then it is computed only once. This
-reduction is efficient for reducing expressions with dead code. For
-instance, the proofs of a proposition {\tt exists~$x$. $P(x)$} reduce to a
-pair of a witness $t$, and a proof that $t$ satisfies the predicate
-$P$. Most of the time, $t$ may be computed without computing the proof
-of $P(t)$, thanks to the lazy strategy.
+Normalization according to the flags is done by first evaluating the
+head of the expression into a {\em weak-head} normal form, i.e. until
+the evaluation is bloked by a variable (or an opaque constant, or an
+axiom), as e.g. in {\tt x\;u$_1$\;...\;u$_n$}, or {\tt match x with
+  ... end}, or {\tt (fix f x \{struct x\} := ...) x}, or is a
+constructed form (a $\lambda$-expression, a constructor, a cofixpoint,
+an inductive type, a product type, a sort), or is a redex that the
+flags prevent to reduce. Once a weak-head normal form is obtained,
+subterms are recursively reduced using the same strategy.
+
+Reduction to weak-head normal form can be done using two strategies:
+{\em lazy} ({\tt lazy} tactic), or {\em call-by-value} ({\tt cbv}
+tactic). The lazy strategy is a call-by-need strategy, with sharing of
+reductions: the arguments of a function call are weakly evaluated only
+when necessary, and if an argument is used several times then it is
+weakly computed only once. This reduction is efficient for reducing
+expressions with dead code. For instance, the proofs of a proposition
+{\tt exists~$x$. $P(x)$} reduce to a pair of a witness $t$, and a
+proof that $t$ satisfies the predicate $P$. Most of the time, $t$ may
+be computed without computing the proof of $P(t)$, thanks to the lazy
+strategy.
 
 The call-by-value strategy is the one used in ML languages: the
-arguments of a function call are evaluated first, using a weak
-reduction (no reduction under the $\lambda$-abstractions). Despite the
-lazy strategy always performs fewer reductions than the call-by-value
-strategy, the latter is generally more efficient for evaluating purely
-computational expressions (i.e. with few dead code).
+arguments of a function call are systematically weakly evaluated
+first. Despite the lazy strategy always performs fewer reductions than
+the call-by-value strategy, the latter is generally more efficient for
+evaluating purely computational expressions (i.e. with few dead code).
 
 \begin{Variants}
 \item {\tt compute} \tacindex{compute}\\
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index a8bbdeb37..a12983ab8 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -477,13 +477,6 @@ through the <tt>Require Import</tt> command.</p>
     theories/MSets/MSetPositive.v
     theories/MSets/MSetToFiniteSet.v
     (theories/MSets/MSets.v)
-    theories/MMaps/MMapAVL.v
-    theories/MMaps/MMapFacts.v
-    theories/MMaps/MMapInterface.v
-    theories/MMaps/MMapList.v
-    theories/MMaps/MMapPositive.v
-    theories/MMaps/MMapWeakList.v
-    (theories/MMaps/MMaps.v)
   </dd>
 
   <dt> <b>FSets</b>: