Merge branch 'v8.5' into trunk

12 files changed, 121 insertions, 118 deletions

diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index e802398b55..76bcaaae67 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -5,7 +5,7 @@
 
 We present here the \Program\ tactic commands, used to build certified
 \Coq\ programs, elaborating them from their algorithmic skeleton and a
-rich specification \cite{Sozeau06}. It can be sought of as a dual of extraction
+rich specification \cite{Sozeau06}. It can be thought of as a dual of extraction
 (see Chapter~\ref{Extraction}). The goal of \Program~is to program as in a regular
 functional programming language whilst using as rich a specification as 
 desired and proving that the code meets the specification using the whole \Coq{} proof
@@ -48,7 +48,7 @@ operation (see Section~\ref{Caseexpr}).
   | S n => u
   end.
 \end{coq_example*}
-will be first rewrote to:
+will be first rewritten to:
 \begin{coq_example*}
   (match x as y return (x = y -> _) with
   | 0 => fun H : x = 0 -> t
@@ -108,7 +108,7 @@ goals to construct the final definitions.
 \subsection{\tt Program Definition {\ident} := {\term}.
   \comindex{Program Definition}\label{ProgramDefinition}}
 
-This command types the value {\term} in \Russell\ and generate proof
+This command types the value {\term} in \Russell\ and generates proof
 obligations. Once solved using the commands shown below, it binds the final
 \Coq\ term to the name {\ident} in the environment.
 
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 49bcdb1db7..6335dfd324 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -29,9 +29,9 @@ for your platform, which is supposed in the following). By default,
 \verb!coqc! executes the native-code version; this can be overridden
 using the \verb!-byte! option.
 
-The byte-code toplevel is based on a Caml
+The byte-code toplevel is based on an {\ocaml}
 toplevel (to allow the dynamic link of tactics).  You can switch to
-the Caml toplevel with the command \verb!Drop.!, and come back to the
+the {\ocaml} toplevel with the command \verb!Drop.!, and come back to the
 \Coq~toplevel with the command \verb!Toplevel.loop();;!.
 
 \section{Batch compilation ({\tt coqc})}
@@ -69,13 +69,13 @@ option \verb:-q:.
 
 Load path can be specified to the \Coq\ system by setting up
 \verb:$COQPATH: environment variable. It is a list of directories
-separated by \verb|:| (\verb|;| on windows). {\Coq} will also honour
-\verb:$XDG_DATA_HOME: and \verb:$XDG_DATA_DIRS: (see section
+separated by \verb|:| (\verb|;| on windows). {\Coq} will also honor
+\verb:$XDG_DATA_HOME: and \verb:$XDG_DATA_DIRS: (see Section
 \ref{loadpath}).
 
 Some {\Coq} commands call other {\Coq} commands. In this case, they
 look for the commands in directory specified by \verb:$COQBIN:. If
-this variable is not set, they look for the command in the executable
+this variable is not set, they look for the commands in the executable
 path.
 
 The \verb:$COQ_COLORS: environment variable can be used to specify the set of
@@ -104,16 +104,16 @@ Add physical path {\em directory} to the {\ocaml} loadpath.
 
   Add physical path \emph{directory} to the list of directories where
   {\Coq} looks for a file and bind it to the the logical directory
-  \emph{dirpath}. The sub-directory structure of \emph{directory} is
+  \emph{dirpath}. The subdirectory structure of \emph{directory} is
   recursively available from {\Coq} using absolute names (extending
   the {\dirpath} prefix) (see Section~\ref{LongNames}).
-  
+
   \SeeAlso Section~\ref{Libraries}.
 
-\item[{\tt -R} {\em directory} {\dirpath}, {\tt -R} {\em directory} [{\tt -as} {\dirpath}]]\
+\item[{\tt -R} {\em directory} {\dirpath}]\
 
   Do as \texttt{-Q} \emph{directory} {\dirpath} but make the
-  sub-directory structure of \emph{directory} recursively visible so
+  subdirectory structure of \emph{directory} recursively visible so
   that the recursive contents of physical \emph{directory} is available
   from {\Coq} using short or partially qualified names.
   
@@ -126,9 +126,9 @@ Add physical path {\em directory} to the {\ocaml} loadpath.
 
 \item[{\tt -exclude-dir} {\em subdirectory}]\ 
 
-  This tells to exclude any sub-directory named {\em subdirectory}
+  This tells to exclude any subdirectory named {\em subdirectory}
   while processing option {\tt -R}. Without this option only the
-  conventional version control management sub-directories named {\tt
+  conventional version control management subdirectories named {\tt
   CVS} and {\tt \_darcs} are excluded.
 
 \item[{\tt -nois}]\ 
@@ -142,11 +142,11 @@ Add physical path {\em directory} to the {\ocaml} loadpath.
 
 \item[{\tt -load-ml-source} {\em file}]\ 
 
-  Load the Caml source file {\em file}.
+  Load the {\ocaml} source file {\em file}.
 
 \item[{\tt -load-ml-object} {\em file}]\ 
 
-  Load the Caml object file {\em file}.
+  Load the {\ocaml} object file {\em file}.
 
 \item[{\tt -l[v]} {\em file}, {\tt -load-vernac-source[-verbose]} {\em file}]\ 
 
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index d1ce3bf41d..cc5239a779 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1059,44 +1059,53 @@ names to {\Coq} names is needed. In this translation, names in the
 file system are called {\em physical} paths while {\Coq} names are
 contrastingly called {\em logical} names.
 
-A logical name {\tt Lib} can associated to a physical path
+A logical prefix {\tt Lib} can be associated to a physical path
 \textrm{\textsl{path}} using the command line option {\tt -Q}
-\textrm{\textsl{path}} {\tt Lib}. This associates a logical name to
-all the compiled files in the directory tree rooted at
-\textrm{\textsl{path}}. The name associated to the file {\tt
-  path/fOO/Bar/File.vo} is {\tt Lib.fOO.Bar.File}. Subdirectories
+\textrm{\textsl{path}} {\tt Lib}. All subfolders of {\textsl{path}} are
+recursively associated to the logical path {\tt Lib} extended with the
+corresponding suffix coming from the physical path. For instance, the
+folder {\tt path/fOO/Bar} maps to {\tt Lib.fOO.Bar}. Subdirectories
 corresponding to invalid {\Coq} identifiers are skipped, and, by
 convention, subdirectories named {\tt CVS} or {\tt \_darcs} are
 skipped too.
 
-{\Coq} commands also associate automatically a logical path to files
+Thanks to this mechanism, {\texttt{.vo}} files are made available through the
+logical name of the folder they are in, extended with their own basename. For
+example, the name associated to the file {\tt path/fOO/Bar/File.vo} is
+{\tt Lib.fOO.Bar.File}. The same caveat applies for invalid identifiers.
+When compiling a source file, the {\texttt{.vo}} file stores its logical name,
+so that an error is issued if it is loaded with the wrong loadpath afterwards.
+
+Some folders have a special status and are automatically put in the path.
+{\Coq} commands associate automatically a logical path to files
 in the repository trees rooted at the directory from where the command
 is launched, \textit{coqlib}\texttt{/user-contrib/}, the directories
 listed in the \verb:$COQPATH:, \verb:${XDG_DATA_HOME}/coq/: and
 \verb:${XDG_DATA_DIRS}/coq/: environment variables (see
 \url{http://standards.freedesktop.org/basedir-spec/basedir-spec-latest.html})
-with the same $/ \to .$ convention but no prefix.
-
-The command line option \texttt{-R} is a variant of \texttt{-Q} that
-associates to a physical path the same logical path as \texttt{-Q}, as
-well as all suffixes of that logical path. The option \texttt{-R}
-\textrm{\textsl{path}} \texttt{Lib} associates to
-\texttt{path/fOO/Bar/File.vo} the logical names
-\texttt{Lib.fOO.Bar.File}, \texttt{fOO.Bar.File}, \texttt{Bar.File}
-and \texttt{File}. If several files with identical base name are
-present in different subdirectories of a recursive loadpath, which of
+with the same physical-to-logical translation and with an empty logical prefix.
+
+The command line option \texttt{-R} is a variant of \texttt{-Q} which has the
+strictly same behavior regarding loadpaths, but which also makes the
+corresponding \texttt{.vo} files available through their short names in a
+way not unlike the {\tt Import} command (see~{\ref{Import}}). For instance,
+\texttt{-R} \textrm{\textsl{path}} \texttt{Lib} associates to the file
+\texttt{path/fOO/Bar/File.vo} the logical name \texttt{Lib.fOO.Bar.File}, but
+allows this file to be accessed through the short names \texttt{fOO.Bar.File},
+\texttt{Bar.File} and \texttt{File}. If several files with identical base name
+are present in different subdirectories of a recursive loadpath, which of
 these files is found first may be system-dependent and explicit
-qualification is recommended.
-
-There are currently two loadpaths in {\Coq}. There is one loadpath
-where seeking {\Coq} files (extensions \texttt{.v} or \texttt{.vo} or
-\texttt{.vi}) whose management has been explained just above, and one
-where seeking {\ocaml} files. The {\ocaml} loadpath is
-managed using the option \texttt{-I path}. As in {\ocaml} world, there
-is nether a notion of logical name prefix nor a way to access files in
-subdirectories of \texttt{path}. See the command \texttt{Declare ML
-  Module} in Section~\ref{compiled} to understand the need of the
-{\ocaml} loadpath.
+qualification is recommended. The {\tt From} argument of the {\tt Require}
+command can be used to bypass the implicit shortening by providing an absolute
+root to the required file (see~\ref{Require}).
+
+There also exists another independent loadpath mechanism attached to {\ocaml}
+object files (\texttt{.cmo} or \texttt{.cmxs}) rather than {\Coq} object files
+as described above. The {\ocaml} loadpath is managed using the option
+\texttt{-I path} (in the {\ocaml} world, there is neither a notion of logical
+name prefix nor a way to access files in subdirectories of \texttt{path}).
+See the command \texttt{Declare ML Module} in Section~\ref{compiled} to
+understand the need of the {\ocaml} loadpath.
 
 See Section~\ref{coqoptions} for a more general view over the {\Coq}
 command line options.
diff --git a/doc/refman/RefMan-mod.tex b/doc/refman/RefMan-mod.tex
index 48b9315e37..e56c8fa7fe 100644
--- a/doc/refman/RefMan-mod.tex
+++ b/doc/refman/RefMan-mod.tex
@@ -3,7 +3,7 @@
 \label{section:Modules}}
 
 The module system provides a way of packaging related elements
-together, as well as a mean of massive abstraction.
+together, as well as a means of massive abstraction.
 
 \begin{figure}[t]
 \begin{centerframe}
diff --git a/doc/refman/RefMan-modr.tex b/doc/refman/RefMan-modr.tex
index 9ab8aded9c..2019a529fe 100644
--- a/doc/refman/RefMan-modr.tex
+++ b/doc/refman/RefMan-modr.tex
@@ -2,7 +2,7 @@
 
 The module system extends the Calculus of Inductive Constructions
 providing a convenient way to structure large developments as well as
-a mean of massive abstraction.
+a means of massive abstraction.
 %It is described in details in Judicael's thesis and Jacek's thesis
 
 \section{Modules and module types}
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 556a2dab58..4952ed7785 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -4,7 +4,7 @@
 \section{Displaying}
 
 \subsection[\tt Print {\qualid}.]{\tt Print {\qualid}.\comindex{Print}}
-This command displays on the screen informations about the declared or
+This command displays on the screen information about the declared or
 defined object referred by {\qualid}.
 
 \begin{ErrMsgs}
@@ -20,7 +20,7 @@ global constant.
 \item {\tt About {\qualid}.}
 \label{About}
 \comindex{About}\\ 
-This displays various informations about the object denoted by {\qualid}:
+This displays various information about the object denoted by {\qualid}:
 its kind (module, constant, assumption, inductive,
 constructor, abbreviation, \ldots), long name, type, implicit
 arguments and argument scopes. It does not print the body of
@@ -34,7 +34,7 @@ definitions or proofs.
 \end{Variants}
 
 \subsection[\tt Print All.]{\tt Print All.\comindex{Print All}}
-This command displays informations about the current state of the
+This command displays information about the current state of the
 environment, including sections and modules.
 
 \begin{Variants}
@@ -183,7 +183,7 @@ displayed as in \Coq\ terms.
 \begin{Variants}
 \item \texttt{Recursive Extraction} {\qualid$_1$} \ldots{} {\qualid$_n$}{\tt .}\\
   Recursively extracts all the material needed for the extraction of 
-  globals {\qualid$_1$}, \ldots, {\qualid$_n$}.
+  global {\qualid$_1$}, \ldots, {\qualid$_n$}.
 \end{Variants}
 
 \SeeAlso Chapter~\ref{Extraction}.
@@ -294,7 +294,7 @@ Search "+"%Z "*"%Z "distr" -positive -Prop.
 Search (?x * _ + ?x * _)%Z outside OmegaLemmas.
 \end{coq_example}
 
-\Warning \comindex{SearchAbout} Up to Coq version 8.4, {\tt Search}
+\Warning \comindex{SearchAbout} Up to {\Coq} version 8.4, {\tt Search}
 had the behavior of current {\tt SearchHead} and the behavior of
 current {\tt Search} was obtained with command {\tt SearchAbout}. For
 compatibility, the deprecated name {\tt SearchAbout} can still be used
@@ -343,7 +343,7 @@ No module \module{} has been required (see Section~\ref{Require}).
 
 \end{Variants}
 
-\Warning Up to Coq version 8.4, {\tt SearchHead} was named {\tt Search}.
+\Warning Up to {\Coq} version 8.4, {\tt SearchHead} was named {\tt Search}.
 
 \subsection[\tt SearchPattern {\termpattern}.]{\tt SearchPattern {\term}.\comindex{SearchPattern}}
 
@@ -458,8 +458,8 @@ The default blacklisted substrings are {\tt
 \label{Locate}}
 This command displays the full name of objects whose name is a prefix of the
 qualified identifier {\qualid}, and consequently the \Coq\ module in which they
-are defined. It searches for objects from the different qualified namespaces of
-Coq: terms, modules, Ltac, etc.
+are defined. It searches for objects from the different qualified name spaces of
+{\Coq}: terms, modules, Ltac, etc.
 
 \begin{coq_eval}
 (*************** The last line should produce **************************)
@@ -553,10 +553,11 @@ the form {\dirpath}{\tt .}{\textsl{ident}} and the file {\ident}{\tt
 mapped in {\Coq} loadpath to the logical path {\dirpath} (see
 Section~\ref{loadpath}). The mapping between physical directories and
 logical names at the time of requiring the file must be consistent
-with the mapping used to compile the file.
+with the mapping used to compile the file. If several files match, one of them
+is picked in an unspecified fashion.
 
 \begin{Variants}
-\item {\tt Require Import {\qualid}.} \comindex{Require} 
+\item {\tt Require Import {\qualid}.} \comindex{Require Import}
 
   This loads and declares the module {\qualid} and its dependencies
   then imports the contents of {\qualid} as described in
@@ -585,6 +586,15 @@ with the mapping used to compile the file.
   given, it also imports {\qualid}$_1$, \ldots, {\qualid}$_n$ and all
   the recursive dependencies that were marked or transitively marked
   as {\tt Export}.
+
+\item {\tt From {\dirpath} Require {\qualid}.}
+  \comindex{From Require}
+
+  This command acts as {\tt Require}, but picks any library whose absolute name
+  is of the form {\tt{\dirpath}.{\dirpath'}.{\qualid}} for some {\dirpath'}.
+  This is useful to ensure that the {\qualid} library comes from a given
+  package by making explicit its absolute root.
+
 \end{Variants}
 
 \begin{ErrMsgs}
@@ -610,7 +620,7 @@ with the mapping used to compile the file.
   \index{Bad-magic-number@{\tt Bad Magic Number}}
   The file {\tt{\ident}.vo} was found but either it is not a \Coq\
   compiled module, or it was compiled with an older and incompatible
-  version of \Coq.
+  version of {\Coq}.
 
 \item \errindex{The file {\ident}.vo contains library {\dirpath} and not
   library {\dirpath'}}
@@ -647,7 +657,7 @@ searched into the current {\ocaml} loadpath (see the command {\tt
 Add ML Path} in the Section~\ref{loadpath}).  Loading of {\ocaml}
 files is only possible under the bytecode version of {\tt coqtop}
 (i.e. {\tt coqtop} called with options {\tt -byte}, see chapter 
-\ref{Addoc-coqc}), or when Coq has been compiled with a version of
+\ref{Addoc-coqc}), or when {\Coq} has been compiled with a version of
 {\ocaml} that supports native {\tt Dynlink} ($\ge$ 3.11).
 
 \begin{Variants}
@@ -658,7 +668,7 @@ files is only possible under the bytecode version of {\tt coqtop}
 
 \begin{ErrMsgs}
 \item \errindex{File not found on loadpath : \str}
-\item \errindex{Loading of ML object file forbidden in a native Coq}
+\item \errindex{Loading of ML object file forbidden in a native {\Coq}}
 \end{ErrMsgs}
 
 \subsection[\tt Print ML Modules.]{\tt Print ML Modules.\comindex{Print ML Modules}}
@@ -669,7 +679,7 @@ should use the command \texttt{Locate File} (see Section~\ref{Locate File})
 \section[Loadpath]{Loadpath}
 
 Loadpaths are preferably managed using {\Coq} command line options
-(see Section~\ref{loadpath}) but there remains vernacular commands to
+(see Section~\ref{loadpath}) but there remain vernacular commands to
 manage them.
 
 \subsection[\tt Pwd.]{\tt Pwd.\comindex{Pwd}\label{Pwd}}
@@ -686,7 +696,7 @@ which can be any valid path.
 
 \subsection[\tt Add LoadPath {\str} as {\dirpath}.]{\tt Add LoadPath {\str} as {\dirpath}.\comindex{Add LoadPath}\label{AddLoadPath}}
 
-This command is equivament to the command line option {\tt -Q {\dirpath}
+This command is equivalent to the command line option {\tt -Q {\dirpath}
   {\str}}. It adds the physical directory {\str} to the current {\Coq}
 loadpath and maps it to the logical directory {\dirpath}.
 
@@ -768,11 +778,11 @@ over the name of a module or of an object inside a module.
 
 This commands undoes all the effects of the last vernacular
 command. Commands read from a vernacular file via a {\tt Load} are
-considered as a single command. Proof managment commands
+considered as a single command. Proof management commands
 are also handled by this command (see Chapter~\ref{Proof-handling}).
 For that, {\tt Back} may have to undo more than one command in order
-to reach a state where the proof managment information is available.
-For instance, when the last command is a {\tt Qed}, the managment
+to reach a state where the proof management information is available.
+For instance, when the last command is a {\tt Qed}, the management
 information about the closed proof has been discarded. In this case,
 {\tt Back} will then undo all the proof steps up to the statement of
 this proof.
@@ -793,7 +803,7 @@ this proof.
 \subsection[\tt BackTo $\num$.]{\tt BackTo $\num$.\comindex{BackTo}}
 \label{sec:statenums}
 
-This command brings back the system to the state labelled $\num$,
+This command brings back the system to the state labeled $\num$,
 forgetting the effect of all commands executed after this state.
 The state label is an integer which grows after each successful command.
 It is displayed in the prompt when in \texttt{-emacs} mode.
@@ -804,14 +814,14 @@ extra commands and end on a state $\num' \leq \num$ if necessary.
 \begin{Variants}
 \item {\tt Backtrack $\num_1$ $\num_2$ $\num_3$}.\comindex{Backtrack}\\
   {\tt Backtrack} is a \emph{deprecated} form of {\tt BackTo} which
-  allows explicitely manipulating the proof environment. The three
+  allows explicitly manipulating the proof environment. The three
   numbers $\num_1$, $\num_2$ and $\num_3$ represent the following:
 \begin{itemize}
 \item $\num_3$: Number of \texttt{Abort} to perform, i.e. the number
   of currently opened nested proofs that must be canceled (see
   Chapter~\ref{Proof-handling}).
 \item $\num_2$: \emph{Proof state number} to unbury once aborts have
-  been done. Coq will compute the number of \texttt{Undo} to perform
+  been done. {\Coq} will compute the number of \texttt{Undo} to perform
   (see Chapter~\ref{Proof-handling}).
 \item $\num_1$: State label to reach, as for {\tt BackTo}.
 \end{itemize}
@@ -939,7 +949,7 @@ algorithm that first normalizes the terms before comparing them.  The
 second algorithm is based on a bytecode representation of terms
 similar to the bytecode representation used in the ZINC virtual
 machine~\cite{Leroy90}. It is especially useful for intensive
-computation of algebraic values, such as numbers, and for reflexion-based
+computation of algebraic values, such as numbers, and for reflection-based
 tactics. The commands to fine-tune the reduction strategies and the
 lazy conversion algorithm are described first.
 
diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex
index 76e4efd606..94290bc80f 100644
--- a/doc/refman/RefMan-uti.tex
+++ b/doc/refman/RefMan-uti.tex
@@ -113,7 +113,7 @@ subdirectory. A specified subdirectory must have an inner
 \texttt{Makefile}. The phony targets \texttt{all} and \texttt{clean}
 will recursively call this target in all the subdirectories.
 
-\item \texttt{-R} and \texttt{-I} options are for {\Coq}, \texttt{-I}
+\item \texttt{-R} and \texttt{-Q} options are for {\Coq}, \texttt{-I}
   for {\ocaml}. The same directory may be ``included'' by both.
 
   Using \texttt{-R} or \texttt{-Q} gives a correct logical path
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 01ad0f70fa..907b30b3e0 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -134,24 +134,17 @@ Options A and B of the licence are {\em not} elected.}
 \bibliography{biblio}
 \cutname{biblio.html}
 
-\printindex
-\cutname{general-index.html}
-
-\printindex[tactic]
-\cutname{tactic-index.html}
-
-\printindex[command]
-\cutname{command-index.html}
-
-\printindex[option]
-\cutname{option-index.html}
-
-\printindex[error]
-\cutname{error-index.html}
+\printrefmanindex{default}{Global Index}{general-index.html}
+\printrefmanindex{tactic}{Tactics Index}{tactic-index.html}
+\printrefmanindex{command}{Vernacular Commands Index}{command-index.html}
+\printrefmanindex{option}{Vernacular Options Index}{option-index.html}
+\printrefmanindex{error}{Index of Error Messages}{error-index.html}
 
 %BEGIN LATEX
-\listoffigures
+\cleardoublepage
+\phantomsection
 \addcontentsline{toc}{chapter}{\listfigurename}
+\listoffigures
 %END LATEX
 
 \end{document}
diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex
index b42480a569..ee2b042f4e 100644
--- a/doc/refman/coqdoc.tex
+++ b/doc/refman/coqdoc.tex
@@ -141,7 +141,7 @@ Example:
 \end{verbatim}
 
 \paragraph{Rules.}
-More than 4 leading dashes produce an horizontal rule.
+More than 4 leading dashes produce a horizontal rule.
 
 \paragraph{Emphasis.}
 Text can be italicized by placing it in underscores.  A non-identifier
diff --git a/doc/refman/headers.hva b/doc/refman/headers.hva
index df4aec272f..9714a29beb 100644
--- a/doc/refman/headers.hva
+++ b/doc/refman/headers.hva
@@ -8,23 +8,19 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \usepackage{index}
 \makeindex
-\newindex{tactic}{tacidx}{tacind}{%
-\protect\addcontentsline{toc}{chapter}{Tactics Index}Tactics Index}
 
-\newindex{command}{comidx}{comind}{%
-\protect\addcontentsline{toc}{chapter}{Vernacular Commands Index}%
-Vernacular Commands Index}
 
-\newindex{option}{optidx}{optind}{%
-\protect\addcontentsline{toc}{chapter}{Vernacular Options Index}%
-Vernacular Options Index}
+\newindex{tactic}{tacidx}{tacind}{Tactics Index}
+\newindex{command}{comidx}{comind}{Vernacular Commands Index}
+\newindex{option}{optidx}{optind}{Vernacular Options Index}
+\newindex{error}{erridx}{errind}{Index of Error Messages}
+\renewindex{default}{idx}{ind}{Global Index}
 
-\newindex{error}{erridx}{errind}{%
-\protect\addcontentsline{toc}{chapter}{Index of Error Messages}Index of Error Messages}
-
-\renewindex{default}{idx}{ind}{%
-\protect\addcontentsline{toc}{chapter}{Global Index}%
-Global Index}
+\newcommand{\printrefmanindex}[3]{%
+\addcontentsline{toc}{chapter}{#2}%
+\printindex[#1]%
+\cutname{#3}%
+}
 
 \newcommand{\tacindex}[1]{%
 \index{#1@\texttt{#1}}\index[tactic]{#1@\texttt{#1}}}
diff --git a/doc/refman/headers.sty b/doc/refman/headers.sty
index ef28588e3c..fb39f687d7 100644
--- a/doc/refman/headers.sty
+++ b/doc/refman/headers.sty
@@ -30,27 +30,21 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \usepackage{index}
 \makeindex
-\newindex{tactic}{tacidx}{tacind}{%
-\protect\setheaders{Tactics Index}%
-\protect\addcontentsline{toc}{chapter}{Tactics Index}Tactics Index}
 
-\newindex{command}{comidx}{comind}{%
-\protect\setheaders{Vernacular Commands Index}%
-\protect\addcontentsline{toc}{chapter}{Vernacular Commands Index}%
-Vernacular Commands Index}
-
-\newindex{option}{optidx}{optind}{%
-\protect\setheaders{Vernacular Options Index}%
-\protect\addcontentsline{toc}{chapter}{Vernacular Options Index}%
-Vernacular Options Index}
-
-\newindex{error}{erridx}{errind}{%
-\protect\setheaders{Index of Error Messages}%
-\protect\addcontentsline{toc}{chapter}{Index of Error Messages}Index of Error Messages}
-
-\renewindex{default}{idx}{ind}{%
-\protect\addcontentsline{toc}{chapter}{Global Index}%
-\protect\setheaders{Global Index}Global Index}
+\newindex{tactic}{tacidx}{tacind}{Tactics Index}
+\newindex{command}{comidx}{comind}{Vernacular Commands Index}
+\newindex{option}{optidx}{optind}{Vernacular Options Index}
+\newindex{error}{erridx}{errind}{Index of Error Messages}
+\renewindex{default}{idx}{ind}{Global Index}
+
+\newcommand{\printrefmanindex}[3]{%
+\cleardoublepage%
+\phantomsection%
+\setheaders{#2}%
+\addcontentsline{toc}{chapter}{#2}%
+\printindex[#1]%
+\cutname{#3}%
+}
 
 \newcommand{\tacindex}[1]{%
 \index{#1@\texttt{#1}}\index[tactic]{#1@\texttt{#1}}}
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 159f8df7f2..024e13413a 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -476,6 +476,7 @@ 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