Merge branch 'v8.5'

2 files changed, 9 insertions, 3 deletions

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 186bc9add3..d388840df5 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1009,7 +1009,7 @@ Fail all:let n:= numgoals in guard n=2.
 Reset Initial.
 \end{coq_eval}
 
-\subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract}\comindex{Qed export}
+\subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract}\comindex{Qed exporting}
 \index{Tacticals!abstract@{\tt abstract}}}
 
 From the outside ``\texttt{abstract \tacexpr}'' is the same as
@@ -1017,9 +1017,9 @@ From the outside ``\texttt{abstract \tacexpr}'' is the same as
 {\ident}\texttt{\_subproof}\textit{n} where {\ident} is the name of the
 current goal and \textit{n} is chosen so that this is a fresh name.
 Such auxiliary lemma is inlined in the final proof term
-unless the proof is ended with ``\texttt{Qed export}''.  In such
+unless the proof is ended with ``\texttt{Qed exporting}''.  In such
 case the lemma is preserved.  The syntax
-``\texttt{Qed export }\ident$_1$\texttt{, ..., }\ident$_n$''
+``\texttt{Qed exporting }\ident$_1$\texttt{, ..., }\ident$_n$''
 is also supported.  In such case the system checks that the names given by the
 user actually exist when the proof is ended.
 
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 854c786c18..159f8df7f2 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -476,6 +476,12 @@ through the <tt>Require Import</tt> command.</p>
     theories/MSets/MSetPositive.v
     theories/MSets/MSetToFiniteSet.v
     (theories/MSets/MSets.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>: